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  1907  ceqex  2943  sbcn1  3089  sbcim1  3090  sbcbi1  3091  sbcel21v  3106  ifnetruedc  3665  peano2  4716  sotri  5157  relcoi1  5293  f0rn0  5561  f1ocnv  5626  tz6.12c  5699  funbrfv  5712  fnbrfvb  5714  fvmptss2  5751  elfvmptrab1  5771  oprabid  6081  eloprabga  6139  elovmporab  6253  elovmporab1w  6254  relmptopab  6255  unielxp  6367  f1o2ndf1  6423  cnvoprab  6429  ressuppss  6453  tfrlem1  6538  tfr1onlemaccex  6578  tfrcllemaccex  6591  ecopovtrn  6865  ecopovtrng  6868  findcard2d  7147  findcard2sd  7148  fidcenumlemr  7224  fsuppimp  7244  difinfsn  7390  nnnninfeq2  7419  ismkvnex  7445  cc3  7578  ltexnqi  7720  prcdnql  7795  prcunqu  7796  prnmaxl  7799  prnminu  7800  ltprordil  7900  1idprl  7901  1idpru  7902  ltexprlemm  7911  ltexprlemopu  7914  ltexprlemru  7923  recexgt0sr  8084  mulgt0sr  8089  ltrenn  8166  nnindnn  8204  nnind  9249  nnmulcl  9254  nnnegz  9576  supinfneg  9923  infsupneg  9924  ublbneg  9941  ixxssxr  10229  ixxssixx  10231  iccshftri  10324  iccshftli  10326  iccdili  10328  icccntri  10330  1fv  10469  fzo1fzo0n0  10518  elfzonlteqm1  10551  ssfzo12  10565  exbtwnzlemshrink  10604  flqeqceilz  10676  zmodidfzoimp  10712  modfzo0difsn  10753  frec2uzltd  10761  frec2uzrdg  10767  frecuzrdgg  10774  seq3clss  10829  seq3fveq2  10833  seqfveq2g  10835  seq3shft2  10839  seqshft2g  10840  monoord  10843  seq3split  10846  seqsplitg  10847  seq3caopr3  10849  seqcaopr3g  10850  seq3f1olemp  10873  seqf1oglem2a  10876  seqf1og  10879  seq3id2  10884  seq3homo  10885  seq3z  10886  seqhomog  10888  seqfeq4g  10889  ser3ge0  10894  exp3vallem  10898  modqexp  11024  fihashf1rn  11146  hashfzp1  11184  seq3coll  11207  swrdswrd  11390  pfxccatin12lem2a  11412  pfxccatin12  11418  swrdccat  11420  pfxccat3a  11423  swrdccatin1d  11428  swrdccatin2d  11429  cjre  11560  climeu  11974  climub  12022  fsum2d  12114  fsumabs  12144  fsumiun  12156  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  prodfap0  12224  prodfrecap  12225  ntrivcvgap  12227  fprodabs  12295  fprod2d  12302  dvdsmod0  12472  p1modz1  12473  dvdsmodexp  12474  dvdsabseq  12526  mulsucdiv2z  12564  nno  12585  nn0o  12586  dfgcd2  12703  lcmgcdlem  12767  cncongr2  12794  exprmfct  12828  eulerthlemrprm  12919  eulerthlema  12920  dvdsprmpweqnn  13027  dvdsprmpweqle  13028  pcmpt  13034  ennnfoneleminc  13151  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemhom  13155  nninfdclemlt  13191  setsn0fun  13238  insubm  13687  ghmghmrn  13969  srgpcomp  14123  ringrng  14169  gsumfzfsumlemm  14722  tg2  14912  hmeof1o  15161  tgioo  15406  dvmptfsum  15577  plycolemc  15610  perfectlem2  15855  gausslemma2dlem0i  15917  lgsquad2lem2  15942  2lgslem3  15961  2lgs  15964  2lgsoddprm  15973  umgrnloop  16098  usgredg2vlem2  16205  subgrprop  16241  wlkv  16308  wlkl1loop  16340  wlk1walkdom  16341  uspgr2wlkeqi  16349  wlkres  16361  umgrclwwlkge2  16384  clwwlknp  16399  clwwlkext2edg  16404  clwwlknun  16423  eupth2fi  16461  bdfind  16703  bj-nn0sucALT  16735  nninfsellemqall  16780