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  2931  sbcn1  3077  sbcim1  3078  sbcbi1  3079  sbcel21v  3094  ifnetruedc  3647  peano2  4691  sotri  5130  relcoi1  5266  f0rn0  5528  f1ocnv  5593  tz6.12c  5665  funbrfv  5678  fnbrfvb  5680  fvmptss2  5717  elfvmptrab1  5737  oprabid  6045  eloprabga  6103  elovmporab  6217  elovmporab1w  6218  relmptopab  6219  unielxp  6332  f1o2ndf1  6388  cnvoprab  6394  tfrlem1  6469  tfr1onlemaccex  6509  tfrcllemaccex  6522  ecopovtrn  6796  ecopovtrng  6799  findcard2d  7075  findcard2sd  7076  fidcenumlemr  7148  difinfsn  7293  nnnninfeq2  7322  ismkvnex  7348  cc3  7480  ltexnqi  7622  prcdnql  7697  prcunqu  7698  prnmaxl  7701  prnminu  7702  ltprordil  7802  1idprl  7803  1idpru  7804  ltexprlemm  7813  ltexprlemopu  7816  ltexprlemru  7825  recexgt0sr  7986  mulgt0sr  7991  ltrenn  8068  nnindnn  8106  nnind  9152  nnmulcl  9157  nnnegz  9475  supinfneg  9822  infsupneg  9823  ublbneg  9840  ixxssxr  10128  ixxssixx  10130  iccshftri  10223  iccshftli  10225  iccdili  10227  icccntri  10229  1fv  10367  fzo1fzo0n0  10415  elfzonlteqm1  10448  ssfzo12  10462  exbtwnzlemshrink  10501  flqeqceilz  10573  zmodidfzoimp  10609  modfzo0difsn  10650  frec2uzltd  10658  frec2uzrdg  10664  frecuzrdgg  10671  seq3clss  10726  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  monoord  10740  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  seqcaopr3g  10747  seq3f1olemp  10770  seqf1oglem2a  10773  seqf1og  10776  seq3id2  10781  seq3homo  10782  seq3z  10783  seqhomog  10785  seqfeq4g  10786  ser3ge0  10791  exp3vallem  10795  modqexp  10921  fihashf1rn  11043  hashfzp1  11081  seq3coll  11099  swrdswrd  11279  pfxccatin12lem2a  11301  pfxccatin12  11307  swrdccat  11309  pfxccat3a  11312  swrdccatin1d  11317  swrdccatin2d  11318  cjre  11436  climeu  11850  climub  11898  fsum2d  11989  fsumabs  12019  fsumiun  12031  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  prodfap0  12099  prodfrecap  12100  ntrivcvgap  12102  fprodabs  12170  fprod2d  12177  dvdsmod0  12347  p1modz1  12348  dvdsmodexp  12349  dvdsabseq  12401  mulsucdiv2z  12439  nno  12460  nn0o  12461  dfgcd2  12578  lcmgcdlem  12642  cncongr2  12669  exprmfct  12703  eulerthlemrprm  12794  eulerthlema  12795  dvdsprmpweqnn  12902  dvdsprmpweqle  12903  pcmpt  12909  ennnfoneleminc  13025  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemhom  13029  nninfdclemlt  13065  setsn0fun  13112  insubm  13561  ghmghmrn  13843  srgpcomp  13996  ringrng  14042  gsumfzfsumlemm  14594  tg2  14777  hmeof1o  15026  tgioo  15271  dvmptfsum  15442  plycolemc  15475  perfectlem2  15717  gausslemma2dlem0i  15779  lgsquad2lem2  15804  2lgslem3  15823  2lgs  15826  2lgsoddprm  15835  umgrnloop  15960  usgredg2vlem2  16067  wlkv  16137  wlkl1loop  16169  wlk1walkdom  16170  uspgr2wlkeqi  16178  wlkres  16188  umgrclwwlkge2  16211  clwwlknp  16226  clwwlkext2edg  16231  clwwlknun  16250  bdfind  16491  bj-nn0sucALT  16523  nninfsellemqall  16567