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  4688  sotri  5127  relcoi1  5263  f0rn0  5525  f1ocnv  5590  tz6.12c  5662  funbrfv  5675  fnbrfvb  5677  fvmptss2  5714  elfvmptrab1  5734  oprabid  6042  eloprabga  6100  elovmporab  6214  elovmporab1w  6215  relmptopab  6216  unielxp  6329  f1o2ndf1  6385  cnvoprab  6391  tfrlem1  6465  tfr1onlemaccex  6505  tfrcllemaccex  6518  ecopovtrn  6792  ecopovtrng  6795  findcard2d  7066  findcard2sd  7067  fidcenumlemr  7138  difinfsn  7283  nnnninfeq2  7312  ismkvnex  7338  cc3  7470  ltexnqi  7612  prcdnql  7687  prcunqu  7688  prnmaxl  7691  prnminu  7692  ltprordil  7792  1idprl  7793  1idpru  7794  ltexprlemm  7803  ltexprlemopu  7806  ltexprlemru  7815  recexgt0sr  7976  mulgt0sr  7981  ltrenn  8058  nnindnn  8096  nnind  9142  nnmulcl  9147  nnnegz  9465  supinfneg  9807  infsupneg  9808  ublbneg  9825  ixxssxr  10113  ixxssixx  10115  iccshftri  10208  iccshftli  10210  iccdili  10212  icccntri  10214  1fv  10352  fzo1fzo0n0  10400  elfzonlteqm1  10433  ssfzo12  10447  exbtwnzlemshrink  10485  flqeqceilz  10557  zmodidfzoimp  10593  modfzo0difsn  10634  frec2uzltd  10642  frec2uzrdg  10648  frecuzrdgg  10655  seq3clss  10710  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  monoord  10724  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seqcaopr3g  10731  seq3f1olemp  10754  seqf1oglem2a  10757  seqf1og  10760  seq3id2  10765  seq3homo  10766  seq3z  10767  seqhomog  10769  seqfeq4g  10770  ser3ge0  10775  exp3vallem  10779  modqexp  10905  fihashf1rn  11027  hashfzp1  11064  seq3coll  11082  swrdswrd  11258  pfxccatin12lem2a  11280  pfxccatin12  11286  swrdccat  11288  pfxccat3a  11291  swrdccatin1d  11296  swrdccatin2d  11297  cjre  11414  climeu  11828  climub  11876  fsum2d  11967  fsumabs  11997  fsumiun  12009  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  prodfap0  12077  prodfrecap  12078  ntrivcvgap  12080  fprodabs  12148  fprod2d  12155  dvdsmod0  12325  p1modz1  12326  dvdsmodexp  12327  dvdsabseq  12379  mulsucdiv2z  12417  nno  12438  nn0o  12439  dfgcd2  12556  lcmgcdlem  12620  cncongr2  12647  exprmfct  12681  eulerthlemrprm  12772  eulerthlema  12773  dvdsprmpweqnn  12880  dvdsprmpweqle  12881  pcmpt  12887  ennnfoneleminc  13003  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemhom  13007  nninfdclemlt  13043  setsn0fun  13090  insubm  13539  ghmghmrn  13821  srgpcomp  13974  ringrng  14020  gsumfzfsumlemm  14572  tg2  14755  hmeof1o  15004  tgioo  15249  dvmptfsum  15420  plycolemc  15453  perfectlem2  15695  gausslemma2dlem0i  15757  lgsquad2lem2  15782  2lgslem3  15801  2lgs  15804  2lgsoddprm  15813  umgrnloop  15937  usgredg2vlem2  16042  wlkv  16098  wlkl1loop  16130  wlk1walkdom  16131  uspgr2wlkeqi  16139  wlkres  16149  umgrclwwlkge2  16171  clwwlknp  16185  clwwlkext2edg  16190  bdfind  16418  bj-nn0sucALT  16450  nninfsellemqall  16495