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  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3684  peano2  4740  sotri  5181  relcoi1  5317  f0rn0  5585  f1ocnv  5650  tz6.12c  5723  funbrfv  5736  fnbrfvb  5738  fvmptss2  5777  elfvmptrab1  5797  oprabid  6111  eloprabga  6169  elovmporab  6283  elovmporab1w  6284  relmptopab  6285  unielxp  6402  f1o2ndf1  6458  cnvoprab  6464  ressuppss  6488  tfrlem1  6573  tfr1onlemaccex  6613  tfrcllemaccex  6626  ecopovtrn  6900  ecopovtrng  6903  findcard2d  7189  findcard2sd  7190  fidcenumlemr  7266  fsuppimp  7286  difinfsn  7434  nnnninfeq2  7463  ismkvnex  7489  cc3  7628  ltexnqi  7770  prcdnql  7845  prcunqu  7846  prnmaxl  7849  prnminu  7850  ltprordil  7950  1idprl  7951  1idpru  7952  ltexprlemm  7961  ltexprlemopu  7964  ltexprlemru  7973  recexgt0sr  8134  mulgt0sr  8139  ltrenn  8216  nnindnn  8254  nnind  9303  nnmulcl  9308  nnnegz  9630  supinfneg  9978  infsupneg  9979  ublbneg  9996  ixxssxr  10285  ixxssixx  10287  iccshftri  10380  iccshftli  10382  iccdili  10384  icccntri  10386  1fv  10529  fzo1fzo0n0  10578  elfzonlteqm1  10611  ssfzo12  10625  exbtwnzlemshrink  10666  flqeqceilz  10738  zmodidfzoimp  10774  modfzo0difsn  10815  frec2uzltd  10823  frec2uzrdg  10829  frecuzrdgg  10836  seq3clss  10891  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  monoord  10905  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  seqcaopr3g  10912  seq3f1olemp  10935  seqf1oglem2a  10938  seqf1og  10941  seq3id2  10946  seq3homo  10947  seq3z  10948  seqhomog  10950  seqfeq4g  10951  ser3ge0  10956  exp3vallem  10960  modqexp  11087  fihashf1rn  11210  hashfzp1  11248  seq3coll  11277  swrdswrd  11460  pfxccatin12lem2a  11482  pfxccatin12  11488  swrdccat  11490  pfxccat3a  11493  swrdccatin1d  11498  swrdccatin2d  11499  cjre  11630  climeu  12045  climub  12093  fsum2d  12185  fsumabs  12215  fsumiun  12227  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  prodfap0  12295  prodfrecap  12296  ntrivcvgap  12298  fprodabs  12366  fprod2d  12373  dvdsmod0  12543  p1modz1  12544  dvdsmodexp  12545  dvdsabseq  12597  mulsucdiv2z  12635  nno  12656  nn0o  12657  dfgcd2  12774  lcmgcdlem  12838  cncongr2  12865  exprmfct  12899  eulerthlemrprm  12990  eulerthlema  12991  dvdsprmpweqnn  13098  dvdsprmpweqle  13099  pcmpt  13105  ballotfilemfc0  13215  ennnfoneleminc  13285  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemhom  13289  nninfdclemlt  13325  setsn0fun  13372  insubm  13775  ghmghmrn  14049  srgpcomp  14277  ringrng  14324  tg2  15144  hmeof1o  15393  tgioo  15638  dvmptfsum  15809  plycolemc  15842  perfectlem2  16097  gausslemma2dlem0i  16159  lgsquad2lem2  16184  2lgslem3  16203  2lgs  16206  2lgsoddprm  16215  umgrnloop  16340  usgredg2vlem2  16447  subgrprop  16483  wlkv  16550  wlkl1loop  16582  wlk1walkdom  16583  uspgr2wlkeqi  16591  wlkres  16603  umgrclwwlkge2  16626  clwwlknp  16641  clwwlkext2edg  16646  clwwlknun  16665  eupth2fi  16703  bdfind  16955  bj-nn0sucALT  16987  nninfsellemqall  17032