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  1906  ceqex  2933  sbcn1  3079  sbcim1  3080  sbcbi1  3081  sbcel21v  3096  ifnetruedc  3649  peano2  4693  sotri  5132  relcoi1  5268  f0rn0  5531  f1ocnv  5596  tz6.12c  5669  funbrfv  5682  fnbrfvb  5684  fvmptss2  5721  elfvmptrab1  5741  oprabid  6050  eloprabga  6108  elovmporab  6222  elovmporab1w  6223  relmptopab  6224  unielxp  6337  f1o2ndf1  6393  cnvoprab  6399  tfrlem1  6474  tfr1onlemaccex  6514  tfrcllemaccex  6527  ecopovtrn  6801  ecopovtrng  6804  findcard2d  7080  findcard2sd  7081  fidcenumlemr  7154  difinfsn  7299  nnnninfeq2  7328  ismkvnex  7354  cc3  7487  ltexnqi  7629  prcdnql  7704  prcunqu  7705  prnmaxl  7708  prnminu  7709  ltprordil  7809  1idprl  7810  1idpru  7811  ltexprlemm  7820  ltexprlemopu  7823  ltexprlemru  7832  recexgt0sr  7993  mulgt0sr  7998  ltrenn  8075  nnindnn  8113  nnind  9159  nnmulcl  9164  nnnegz  9482  supinfneg  9829  infsupneg  9830  ublbneg  9847  ixxssxr  10135  ixxssixx  10137  iccshftri  10230  iccshftli  10232  iccdili  10234  icccntri  10236  1fv  10374  fzo1fzo0n0  10423  elfzonlteqm1  10456  ssfzo12  10470  exbtwnzlemshrink  10509  flqeqceilz  10581  zmodidfzoimp  10617  modfzo0difsn  10658  frec2uzltd  10666  frec2uzrdg  10672  frecuzrdgg  10679  seq3clss  10734  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord  10748  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  ser3ge0  10799  exp3vallem  10803  modqexp  10929  fihashf1rn  11051  hashfzp1  11089  seq3coll  11107  swrdswrd  11287  pfxccatin12lem2a  11309  pfxccatin12  11315  swrdccat  11317  pfxccat3a  11320  swrdccatin1d  11325  swrdccatin2d  11326  cjre  11444  climeu  11858  climub  11906  fsum2d  11998  fsumabs  12028  fsumiun  12040  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  prodfap0  12108  prodfrecap  12109  ntrivcvgap  12111  fprodabs  12179  fprod2d  12186  dvdsmod0  12356  p1modz1  12357  dvdsmodexp  12358  dvdsabseq  12410  mulsucdiv2z  12448  nno  12469  nn0o  12470  dfgcd2  12587  lcmgcdlem  12651  cncongr2  12678  exprmfct  12712  eulerthlemrprm  12803  eulerthlema  12804  dvdsprmpweqnn  12911  dvdsprmpweqle  12912  pcmpt  12918  ennnfoneleminc  13034  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemhom  13038  nninfdclemlt  13074  setsn0fun  13121  insubm  13570  ghmghmrn  13852  srgpcomp  14006  ringrng  14052  gsumfzfsumlemm  14604  tg2  14787  hmeof1o  15036  tgioo  15281  dvmptfsum  15452  plycolemc  15485  perfectlem2  15727  gausslemma2dlem0i  15789  lgsquad2lem2  15814  2lgslem3  15833  2lgs  15836  2lgsoddprm  15845  umgrnloop  15970  usgredg2vlem2  16077  subgrprop  16113  wlkv  16180  wlkl1loop  16212  wlk1walkdom  16213  uspgr2wlkeqi  16221  wlkres  16233  umgrclwwlkge2  16256  clwwlknp  16271  clwwlkext2edg  16276  clwwlknun  16295  eupth2fi  16333  bdfind  16562  bj-nn0sucALT  16594  nninfsellemqall  16638