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  1831  ceqex  2816  sbcn1  2960  sbcim1  2961  sbcbi1  2962  sbcel21v  2977  peano2  4517  sotri  4942  relcoi1  5078  f0rn0  5325  f1ocnv  5388  tz6.12c  5459  funbrfv  5468  fnbrfvb  5470  fvmptss2  5504  elfvmptrab1  5523  oprabid  5811  eloprabga  5866  unielxp  6080  f1o2ndf1  6133  cnvoprab  6139  tfrlem1  6213  tfr1onlemaccex  6253  tfrcllemaccex  6266  ecopovtrn  6534  ecopovtrng  6537  findcard2d  6793  findcard2sd  6794  fidcenumlemr  6851  difinfsn  6993  ismkvnex  7037  cc3  7100  ltexnqi  7241  prcdnql  7316  prcunqu  7317  prnmaxl  7320  prnminu  7321  ltprordil  7421  1idprl  7422  1idpru  7423  ltexprlemm  7432  ltexprlemopu  7435  ltexprlemru  7444  recexgt0sr  7605  mulgt0sr  7610  ltrenn  7687  nnindnn  7725  nnind  8760  nnmulcl  8765  nnnegz  9081  supinfneg  9417  infsupneg  9418  ublbneg  9432  ixxssxr  9713  ixxssixx  9715  iccshftri  9808  iccshftli  9810  iccdili  9812  icccntri  9814  1fv  9947  fzo1fzo0n0  9991  elfzonlteqm1  10018  ssfzo12  10032  exbtwnzlemshrink  10057  flqeqceilz  10122  zmodidfzoimp  10158  modfzo0difsn  10199  frec2uzltd  10207  frec2uzrdg  10213  frecuzrdgg  10220  seq3clss  10271  seq3fveq2  10273  seq3shft2  10277  monoord  10280  seq3split  10283  seq3caopr3  10285  seq3f1olemp  10306  seq3id2  10313  seq3homo  10314  seq3z  10315  ser3ge0  10321  exp3vallem  10325  fihashf1rn  10567  hashfzp1  10602  seq3coll  10617  cjre  10686  climeu  11097  climub  11145  fsum2d  11236  fsumabs  11266  fsumiun  11278  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  prodfap0  11346  prodfrecap  11347  ntrivcvgap  11349  dvdsabseq  11581  mulsucdiv2z  11618  nno  11639  nn0o  11640  dfgcd2  11738  lcmgcdlem  11794  cncongr2  11821  exprmfct  11854  ennnfoneleminc  11960  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ennnfonelemhom  11964  setsn0fun  12035  tg2  12268  hmeof1o  12517  tgioo  12754  bdfind  13315  bj-nn0sucALT  13347  nninfsellemqall  13386