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  1872  ceqex  2891  sbcn1  3037  sbcim1  3038  sbcbi1  3039  sbcel21v  3054  ifnetruedc  3602  peano2  4631  sotri  5065  relcoi1  5201  f0rn0  5452  f1ocnv  5517  tz6.12c  5588  funbrfv  5599  fnbrfvb  5601  fvmptss2  5636  elfvmptrab1  5656  oprabid  5954  eloprabga  6009  elovmporab  6123  elovmporab1w  6124  unielxp  6232  f1o2ndf1  6286  cnvoprab  6292  tfrlem1  6366  tfr1onlemaccex  6406  tfrcllemaccex  6419  ecopovtrn  6691  ecopovtrng  6694  findcard2d  6952  findcard2sd  6953  fidcenumlemr  7021  difinfsn  7166  nnnninfeq2  7195  ismkvnex  7221  cc3  7335  ltexnqi  7476  prcdnql  7551  prcunqu  7552  prnmaxl  7555  prnminu  7556  ltprordil  7656  1idprl  7657  1idpru  7658  ltexprlemm  7667  ltexprlemopu  7670  ltexprlemru  7679  recexgt0sr  7840  mulgt0sr  7845  ltrenn  7922  nnindnn  7960  nnind  9006  nnmulcl  9011  nnnegz  9329  supinfneg  9669  infsupneg  9670  ublbneg  9687  ixxssxr  9975  ixxssixx  9977  iccshftri  10070  iccshftli  10072  iccdili  10074  icccntri  10076  1fv  10214  fzo1fzo0n0  10259  elfzonlteqm1  10286  ssfzo12  10300  exbtwnzlemshrink  10338  flqeqceilz  10410  zmodidfzoimp  10446  modfzo0difsn  10487  frec2uzltd  10495  frec2uzrdg  10501  frecuzrdgg  10508  seq3clss  10563  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord  10577  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3f1olemp  10607  seqf1oglem2a  10610  seqf1og  10613  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  ser3ge0  10628  exp3vallem  10632  modqexp  10758  fihashf1rn  10880  hashfzp1  10916  seq3coll  10934  cjre  11047  climeu  11461  climub  11509  fsum2d  11600  fsumabs  11630  fsumiun  11642  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  prodfap0  11710  prodfrecap  11711  ntrivcvgap  11713  fprodabs  11781  fprod2d  11788  dvdsmod0  11958  p1modz1  11959  dvdsmodexp  11960  dvdsabseq  12012  mulsucdiv2z  12050  nno  12071  nn0o  12072  dfgcd2  12181  lcmgcdlem  12245  cncongr2  12272  exprmfct  12306  eulerthlemrprm  12397  eulerthlema  12398  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  pcmpt  12512  ennnfoneleminc  12628  ennnfonelemkh  12629  ennnfonelemhf1o  12630  ennnfonelemhom  12632  nninfdclemlt  12668  setsn0fun  12715  insubm  13117  ghmghmrn  13393  srgpcomp  13546  ringrng  13592  gsumfzfsumlemm  14143  tg2  14296  hmeof1o  14545  tgioo  14790  dvmptfsum  14961  plycolemc  14994  perfectlem2  15236  gausslemma2dlem0i  15298  lgsquad2lem2  15323  2lgslem3  15342  2lgs  15345  2lgsoddprm  15354  bdfind  15592  bj-nn0sucALT  15624  nninfsellemqall  15659