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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syldan  282  ax16i  1904  ceqex  2930  sbcn1  3076  sbcim1  3077  sbcbi1  3078  sbcel21v  3093  ifnetruedc  3646  peano2  4687  sotri  5124  relcoi1  5260  f0rn0  5522  f1ocnv  5587  tz6.12c  5659  funbrfv  5672  fnbrfvb  5674  fvmptss2  5711  elfvmptrab1  5731  oprabid  6039  eloprabga  6097  elovmporab  6211  elovmporab1w  6212  relmptopab  6213  unielxp  6326  f1o2ndf1  6380  cnvoprab  6386  tfrlem1  6460  tfr1onlemaccex  6500  tfrcllemaccex  6513  ecopovtrn  6787  ecopovtrng  6790  findcard2d  7061  findcard2sd  7062  fidcenumlemr  7130  difinfsn  7275  nnnninfeq2  7304  ismkvnex  7330  cc3  7462  ltexnqi  7604  prcdnql  7679  prcunqu  7680  prnmaxl  7683  prnminu  7684  ltprordil  7784  1idprl  7785  1idpru  7786  ltexprlemm  7795  ltexprlemopu  7798  ltexprlemru  7807  recexgt0sr  7968  mulgt0sr  7973  ltrenn  8050  nnindnn  8088  nnind  9134  nnmulcl  9139  nnnegz  9457  supinfneg  9798  infsupneg  9799  ublbneg  9816  ixxssxr  10104  ixxssixx  10106  iccshftri  10199  iccshftli  10201  iccdili  10203  icccntri  10205  1fv  10343  fzo1fzo0n0  10391  elfzonlteqm1  10424  ssfzo12  10438  exbtwnzlemshrink  10476  flqeqceilz  10548  zmodidfzoimp  10584  modfzo0difsn  10625  frec2uzltd  10633  frec2uzrdg  10639  frecuzrdgg  10646  seq3clss  10701  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  monoord  10715  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  seqcaopr3g  10722  seq3f1olemp  10745  seqf1oglem2a  10748  seqf1og  10751  seq3id2  10756  seq3homo  10757  seq3z  10758  seqhomog  10760  seqfeq4g  10761  ser3ge0  10766  exp3vallem  10770  modqexp  10896  fihashf1rn  11018  hashfzp1  11054  seq3coll  11072  swrdswrd  11245  pfxccatin12lem2a  11267  pfxccatin12  11273  swrdccat  11275  pfxccat3a  11278  swrdccatin1d  11283  swrdccatin2d  11284  cjre  11401  climeu  11815  climub  11863  fsum2d  11954  fsumabs  11984  fsumiun  11996  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  prodfap0  12064  prodfrecap  12065  ntrivcvgap  12067  fprodabs  12135  fprod2d  12142  dvdsmod0  12312  p1modz1  12313  dvdsmodexp  12314  dvdsabseq  12366  mulsucdiv2z  12404  nno  12425  nn0o  12426  dfgcd2  12543  lcmgcdlem  12607  cncongr2  12634  exprmfct  12668  eulerthlemrprm  12759  eulerthlema  12760  dvdsprmpweqnn  12867  dvdsprmpweqle  12868  pcmpt  12874  ennnfoneleminc  12990  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemhom  12994  nninfdclemlt  13030  setsn0fun  13077  insubm  13526  ghmghmrn  13808  srgpcomp  13961  ringrng  14007  gsumfzfsumlemm  14559  tg2  14742  hmeof1o  14991  tgioo  15236  dvmptfsum  15407  plycolemc  15440  perfectlem2  15682  gausslemma2dlem0i  15744  lgsquad2lem2  15769  2lgslem3  15788  2lgs  15791  2lgsoddprm  15800  umgrnloop  15924  usgredg2vlem2  16029  wlkv  16047  wlkl1loop  16079  wlk1walkdom  16080  uspgr2wlkeqi  16088  wlkres  16098  bdfind  16333  bj-nn0sucALT  16365  nninfsellemqall  16411