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  1905  ceqex  2932  sbcn1  3078  sbcim1  3079  sbcbi1  3080  sbcel21v  3095  ifnetruedc  3650  peano2  4695  sotri  5134  relcoi1  5270  f0rn0  5534  f1ocnv  5599  tz6.12c  5672  funbrfv  5685  fnbrfvb  5687  fvmptss2  5724  elfvmptrab1  5744  oprabid  6055  eloprabga  6113  elovmporab  6227  elovmporab1w  6228  relmptopab  6229  unielxp  6342  f1o2ndf1  6398  cnvoprab  6404  tfrlem1  6479  tfr1onlemaccex  6519  tfrcllemaccex  6532  ecopovtrn  6806  ecopovtrng  6809  findcard2d  7085  findcard2sd  7086  fidcenumlemr  7159  difinfsn  7304  nnnninfeq2  7333  ismkvnex  7359  cc3  7492  ltexnqi  7634  prcdnql  7709  prcunqu  7710  prnmaxl  7713  prnminu  7714  ltprordil  7814  1idprl  7815  1idpru  7816  ltexprlemm  7825  ltexprlemopu  7828  ltexprlemru  7837  recexgt0sr  7998  mulgt0sr  8003  ltrenn  8080  nnindnn  8118  nnind  9164  nnmulcl  9169  nnnegz  9487  supinfneg  9834  infsupneg  9835  ublbneg  9852  ixxssxr  10140  ixxssixx  10142  iccshftri  10235  iccshftli  10237  iccdili  10239  icccntri  10241  1fv  10379  fzo1fzo0n0  10428  elfzonlteqm1  10461  ssfzo12  10475  exbtwnzlemshrink  10514  flqeqceilz  10586  zmodidfzoimp  10622  modfzo0difsn  10663  frec2uzltd  10671  frec2uzrdg  10677  frecuzrdgg  10684  seq3clss  10739  seq3fveq2  10743  seqfveq2g  10745  seq3shft2  10749  seqshft2g  10750  monoord  10753  seq3split  10756  seqsplitg  10757  seq3caopr3  10759  seqcaopr3g  10760  seq3f1olemp  10783  seqf1oglem2a  10786  seqf1og  10789  seq3id2  10794  seq3homo  10795  seq3z  10796  seqhomog  10798  seqfeq4g  10799  ser3ge0  10804  exp3vallem  10808  modqexp  10934  fihashf1rn  11056  hashfzp1  11094  seq3coll  11112  swrdswrd  11295  pfxccatin12lem2a  11317  pfxccatin12  11323  swrdccat  11325  pfxccat3a  11328  swrdccatin1d  11333  swrdccatin2d  11334  cjre  11465  climeu  11879  climub  11927  fsum2d  12019  fsumabs  12049  fsumiun  12061  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  prodfap0  12129  prodfrecap  12130  ntrivcvgap  12132  fprodabs  12200  fprod2d  12207  dvdsmod0  12377  p1modz1  12378  dvdsmodexp  12379  dvdsabseq  12431  mulsucdiv2z  12469  nno  12490  nn0o  12491  dfgcd2  12608  lcmgcdlem  12672  cncongr2  12699  exprmfct  12733  eulerthlemrprm  12824  eulerthlema  12825  dvdsprmpweqnn  12932  dvdsprmpweqle  12933  pcmpt  12939  ennnfoneleminc  13055  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemhom  13059  nninfdclemlt  13095  setsn0fun  13142  insubm  13591  ghmghmrn  13873  srgpcomp  14027  ringrng  14073  gsumfzfsumlemm  14625  tg2  14813  hmeof1o  15062  tgioo  15307  dvmptfsum  15478  plycolemc  15511  perfectlem2  15753  gausslemma2dlem0i  15815  lgsquad2lem2  15840  2lgslem3  15859  2lgs  15862  2lgsoddprm  15871  umgrnloop  15996  usgredg2vlem2  16103  subgrprop  16139  wlkv  16206  wlkl1loop  16238  wlk1walkdom  16239  uspgr2wlkeqi  16247  wlkres  16259  umgrclwwlkge2  16282  clwwlknp  16297  clwwlkext2edg  16302  clwwlknun  16321  eupth2fi  16359  bdfind  16601  bj-nn0sucALT  16633  nninfsellemqall  16680