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  280  ax16i  1851  ceqex  2857  sbcn1  3002  sbcim1  3003  sbcbi1  3004  sbcel21v  3019  peano2  4579  sotri  5006  relcoi1  5142  f0rn0  5392  f1ocnv  5455  tz6.12c  5526  funbrfv  5535  fnbrfvb  5537  fvmptss2  5571  elfvmptrab1  5590  oprabid  5885  eloprabga  5940  unielxp  6153  f1o2ndf1  6207  cnvoprab  6213  tfrlem1  6287  tfr1onlemaccex  6327  tfrcllemaccex  6340  ecopovtrn  6610  ecopovtrng  6613  findcard2d  6869  findcard2sd  6870  fidcenumlemr  6932  difinfsn  7077  nnnninfeq2  7105  ismkvnex  7131  cc3  7230  ltexnqi  7371  prcdnql  7446  prcunqu  7447  prnmaxl  7450  prnminu  7451  ltprordil  7551  1idprl  7552  1idpru  7553  ltexprlemm  7562  ltexprlemopu  7565  ltexprlemru  7574  recexgt0sr  7735  mulgt0sr  7740  ltrenn  7817  nnindnn  7855  nnind  8894  nnmulcl  8899  nnnegz  9215  supinfneg  9554  infsupneg  9555  ublbneg  9572  ixxssxr  9857  ixxssixx  9859  iccshftri  9952  iccshftli  9954  iccdili  9956  icccntri  9958  1fv  10095  fzo1fzo0n0  10139  elfzonlteqm1  10166  ssfzo12  10180  exbtwnzlemshrink  10205  flqeqceilz  10274  zmodidfzoimp  10310  modfzo0difsn  10351  frec2uzltd  10359  frec2uzrdg  10365  frecuzrdgg  10372  seq3clss  10423  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  seq3caopr3  10437  seq3f1olemp  10458  seq3id2  10465  seq3homo  10466  seq3z  10467  ser3ge0  10473  exp3vallem  10477  modqexp  10602  fihashf1rn  10723  hashfzp1  10759  seq3coll  10777  cjre  10846  climeu  11259  climub  11307  fsum2d  11398  fsumabs  11428  fsumiun  11440  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  prodfap0  11508  prodfrecap  11509  ntrivcvgap  11511  fprodabs  11579  fprod2d  11586  dvdsmod0  11755  p1modz1  11756  dvdsmodexp  11757  dvdsabseq  11807  mulsucdiv2z  11844  nno  11865  nn0o  11866  dfgcd2  11969  lcmgcdlem  12031  cncongr2  12058  exprmfct  12092  eulerthlemrprm  12183  eulerthlema  12184  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  pcmpt  12295  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemhom  12370  nninfdclemlt  12406  setsn0fun  12453  insubm  12703  tg2  12854  hmeof1o  13103  tgioo  13340  bdfind  13981  bj-nn0sucALT  14013  nninfsellemqall  14048