Theorem mpcom 36

Description: Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.)

Hypotheses

Ref	Expression
mpcom.1	⊢ (𝜓 → 𝜑)
mpcom.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpcom	⊢ (𝜓 → 𝜒)

Proof of Theorem mpcom

Step	Hyp	Ref	Expression
1		mpcom.1	. 2 ⊢ (𝜓 → 𝜑)
2		mpcom.2	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	com12 30	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syldan  276  ax16i  1779  ceqex  2722  sbcn1  2861  sbcim1  2862  sbcbi1  2863  sbcel21v  2878  peano2  4336  sotri  4740  relcoi1  4869  f1ocnv  5159  tz6.12c  5224  funbrfv  5233  fnbrfvb  5235  fvmptss2  5268  oprabid  5557  eloprabga  5611  unielxp  5820  f1o2ndf1  5869  cnvoprab  5875  tfrlem1  5946  freccl  6016  ecopovtrn  6226  ecopovtrng  6229  findcard2d  6375  findcard2sd  6376  ltexnqi  6599  prcdnql  6674  prcunqu  6675  prnmaxl  6678  prnminu  6679  ltprordil  6779  1idprl  6780  1idpru  6781  ltexprlemm  6790  ltexprlemopu  6793  ltexprlemru  6802  recexgt0sr  6950  mulgt0sr  6954  ltrenn  7023  nnindnn  7059  nnind  8055  nnmulcl  8060  nnnegz  8354  supinfneg  8683  infsupneg  8684  ublbneg  8698  ixxssxr  8923  ixxssixx  8925  iccshftri  9017  iccshftli  9019  iccdili  9021  icccntri  9023  1fv  9149  fzo1fzo0n0  9192  elfzonlteqm1  9219  ssfzo12  9233  flqeqceilz  9320  zmodidfzoimp  9356  modfzo0difsn  9397  frec2uzltd  9405  frec2uzrdg  9411  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  iseqcaopr3  9460  iseqhomo  9468  iseqz  9469  cjre  9769  climeu  10135  climub  10182  dvdsabseq  10247  mulsucdiv2z  10285  nno  10306  nn0o  10307  dfgcd2  10403  lcmgcdlem  10459  cncongr2  10486  exprmfct  10519  bdfind  10741  bj-nn0sucALT  10773