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 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldan  282  ax16i  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3684  peano2  4742  sotri  5183  relcoi1  5319  f0rn0  5587  f1ocnv  5652  tz6.12c  5725  funbrfv  5739  fnbrfvb  5741  fvmptss2  5780  elfvmptrab1  5801  oprabid  6117  eloprabga  6175  elovmporab  6289  elovmporab1w  6290  relmptopab  6291  unielxp  6408  f1o2ndf1  6464  cnvoprab  6470  ressuppss  6494  tfrlem1  6579  tfr1onlemaccex  6619  tfrcllemaccex  6632  ecopovtrn  6906  ecopovtrng  6909  findcard2d  7195  findcard2sd  7196  fidcenumlemr  7272  fsuppimp  7292  difinfsn  7440  nnnninfeq2  7469  ismkvnex  7495  cc3  7634  ltexnqi  7776  prcdnql  7851  prcunqu  7852  prnmaxl  7855  prnminu  7856  ltprordil  7956  1idprl  7957  1idpru  7958  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemru  7979  recexgt0sr  8140  mulgt0sr  8145  ltrenn  8222  nnindnn  8260  nnind  9321  nnmulcl  9326  nnnegz  9649  supinfneg  9997  infsupneg  9998  ublbneg  10015  ixxssxr  10304  ixxssixx  10306  iccshftri  10399  iccshftli  10401  iccdili  10403  icccntri  10405  1fv  10548  fzo1fzo0n0  10597  elfzonlteqm1  10630  ssfzo12  10644  exbtwnzlemshrink  10685  flqeqceilz  10757  zmodidfzoimp  10793  modfzo0difsn  10834  frec2uzltd  10842  frec2uzrdg  10848  frecuzrdgg  10855  seq3clss  10910  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord  10924  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  seqcaopr3g  10931  seq3f1olemp  10954  seqf1oglem2a  10957  seqf1og  10960  seq3id2  10965  seq3homo  10966  seq3z  10967  seqhomog  10969  seqfeq4g  10970  ser3ge0  10975  exp3vallem  10979  modqexp  11106  fihashf1rn  11229  hashfzp1  11267  seq3coll  11296  swrdswrd  11479  pfxccatin12lem2a  11501  pfxccatin12  11507  swrdccat  11509  pfxccat3a  11512  swrdccatin1d  11517  swrdccatin2d  11518  cjre  11649  climeu  12064  climub  12112  fsum2d  12204  fsumabs  12234  fsumiun  12246  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  prodfap0  12314  prodfrecap  12315  ntrivcvgap  12317  fprodabs  12385  fprod2d  12392  dvdsmod0  12562  p1modz1  12563  dvdsmodexp  12564  dvdsabseq  12616  mulsucdiv2z  12654  nno  12675  nn0o  12676  dfgcd2  12793  lcmgcdlem  12857  cncongr2  12884  exprmfct  12918  eulerthlemrprm  13009  eulerthlema  13010  dvdsprmpweqnn  13117  dvdsprmpweqle  13118  pcmpt  13124  ballotfilemfc0  13234  ennnfoneleminc  13304  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemhom  13308  nninfdclemlt  13344  setsn0fun  13391  insubm  13794  ghmghmrn  14068  srgpcomp  14296  ringrng  14343  tg2  15163  hmeof1o  15412  tgioo  15657  dvmptfsum  15828  plycolemc  15861  perfectlem2  16120  gausslemma2dlem0i  16188  lgsquad2lem2  16213  2lgslem3  16232  2lgs  16235  2lgsoddprm  16244  umgrnloop  16369  usgredg2vlem2  16476  subgrprop  16512  wlkv  16579  wlkl1loop  16611  wlk1walkdom  16612  uspgr2wlkeqi  16620  wlkres  16632  umgrclwwlkge2  16655  clwwlknp  16670  clwwlkext2edg  16675  clwwlknun  16694  eupth2fi  16732  bdfind  16984  bj-nn0sucALT  17016  nninfsellemqall  17070