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  1869  ceqex  2879  sbcn1  3025  sbcim1  3026  sbcbi1  3027  sbcel21v  3042  peano2  4612  sotri  5042  relcoi1  5178  f0rn0  5429  f1ocnv  5493  tz6.12c  5564  funbrfv  5575  fnbrfvb  5577  fvmptss2  5612  elfvmptrab1  5631  oprabid  5929  eloprabga  5984  unielxp  6200  f1o2ndf1  6254  cnvoprab  6260  tfrlem1  6334  tfr1onlemaccex  6374  tfrcllemaccex  6387  ecopovtrn  6659  ecopovtrng  6662  findcard2d  6920  findcard2sd  6921  fidcenumlemr  6985  difinfsn  7130  nnnninfeq2  7158  ismkvnex  7184  cc3  7298  ltexnqi  7439  prcdnql  7514  prcunqu  7515  prnmaxl  7518  prnminu  7519  ltprordil  7619  1idprl  7620  1idpru  7621  ltexprlemm  7630  ltexprlemopu  7633  ltexprlemru  7642  recexgt0sr  7803  mulgt0sr  7808  ltrenn  7885  nnindnn  7923  nnind  8966  nnmulcl  8971  nnnegz  9287  supinfneg  9627  infsupneg  9628  ublbneg  9645  ixxssxr  9932  ixxssixx  9934  iccshftri  10027  iccshftli  10029  iccdili  10031  icccntri  10033  1fv  10171  fzo1fzo0n0  10215  elfzonlteqm1  10242  ssfzo12  10256  exbtwnzlemshrink  10281  flqeqceilz  10351  zmodidfzoimp  10387  modfzo0difsn  10428  frec2uzltd  10436  frec2uzrdg  10442  frecuzrdgg  10449  seq3clss  10500  seq3fveq2  10502  seq3shft2  10506  monoord  10509  seq3split  10512  seq3caopr3  10514  seq3f1olemp  10535  seq3id2  10542  seq3homo  10543  seq3z  10544  seqfeq4g  10546  ser3ge0  10551  exp3vallem  10555  modqexp  10681  fihashf1rn  10803  hashfzp1  10839  seq3coll  10857  cjre  10926  climeu  11339  climub  11387  fsum2d  11478  fsumabs  11508  fsumiun  11520  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  prodfap0  11588  prodfrecap  11589  ntrivcvgap  11591  fprodabs  11659  fprod2d  11666  dvdsmod0  11835  p1modz1  11836  dvdsmodexp  11837  dvdsabseq  11888  mulsucdiv2z  11925  nno  11946  nn0o  11947  dfgcd2  12050  lcmgcdlem  12112  cncongr2  12139  exprmfct  12173  eulerthlemrprm  12264  eulerthlema  12265  dvdsprmpweqnn  12371  dvdsprmpweqle  12372  pcmpt  12378  ennnfoneleminc  12465  ennnfonelemkh  12466  ennnfonelemhf1o  12467  ennnfonelemhom  12469  nninfdclemlt  12505  setsn0fun  12552  insubm  12952  ghmghmrn  13219  srgpcomp  13361  ringrng  13407  tg2  14037  hmeof1o  14286  tgioo  14523  bdfind  15176  bj-nn0sucALT  15208  nninfsellemqall  15243