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  1858  ceqex  2865  sbcn1  3011  sbcim1  3012  sbcbi1  3013  sbcel21v  3028  peano2  4595  sotri  5025  relcoi1  5161  f0rn0  5411  f1ocnv  5475  tz6.12c  5546  funbrfv  5555  fnbrfvb  5557  fvmptss2  5592  elfvmptrab1  5611  oprabid  5907  eloprabga  5962  unielxp  6175  f1o2ndf1  6229  cnvoprab  6235  tfrlem1  6309  tfr1onlemaccex  6349  tfrcllemaccex  6362  ecopovtrn  6632  ecopovtrng  6635  findcard2d  6891  findcard2sd  6892  fidcenumlemr  6954  difinfsn  7099  nnnninfeq2  7127  ismkvnex  7153  cc3  7267  ltexnqi  7408  prcdnql  7483  prcunqu  7484  prnmaxl  7487  prnminu  7488  ltprordil  7588  1idprl  7589  1idpru  7590  ltexprlemm  7599  ltexprlemopu  7602  ltexprlemru  7611  recexgt0sr  7772  mulgt0sr  7777  ltrenn  7854  nnindnn  7892  nnind  8935  nnmulcl  8940  nnnegz  9256  supinfneg  9595  infsupneg  9596  ublbneg  9613  ixxssxr  9900  ixxssixx  9902  iccshftri  9995  iccshftli  9997  iccdili  9999  icccntri  10001  1fv  10139  fzo1fzo0n0  10183  elfzonlteqm1  10210  ssfzo12  10224  exbtwnzlemshrink  10249  flqeqceilz  10318  zmodidfzoimp  10354  modfzo0difsn  10395  frec2uzltd  10403  frec2uzrdg  10409  frecuzrdgg  10416  seq3clss  10467  seq3fveq2  10469  seq3shft2  10473  monoord  10476  seq3split  10479  seq3caopr3  10481  seq3f1olemp  10502  seq3id2  10509  seq3homo  10510  seq3z  10511  ser3ge0  10517  exp3vallem  10521  modqexp  10647  fihashf1rn  10768  hashfzp1  10804  seq3coll  10822  cjre  10891  climeu  11304  climub  11352  fsum2d  11443  fsumabs  11473  fsumiun  11485  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  prodfap0  11553  prodfrecap  11554  ntrivcvgap  11556  fprodabs  11624  fprod2d  11631  dvdsmod0  11800  p1modz1  11801  dvdsmodexp  11802  dvdsabseq  11853  mulsucdiv2z  11890  nno  11911  nn0o  11912  dfgcd2  12015  lcmgcdlem  12077  cncongr2  12104  exprmfct  12138  eulerthlemrprm  12229  eulerthlema  12230  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  pcmpt  12341  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemhom  12416  nninfdclemlt  12452  setsn0fun  12499  insubm  12872  srgpcomp  13173  tg2  13563  hmeof1o  13812  tgioo  14049  bdfind  14701  bj-nn0sucALT  14733  nninfsellemqall  14767