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  3603  peano2  4632  sotri  5066  relcoi1  5202  f0rn0  5455  f1ocnv  5520  tz6.12c  5591  funbrfv  5602  fnbrfvb  5604  fvmptss2  5639  elfvmptrab1  5659  oprabid  5957  eloprabga  6013  elovmporab  6127  elovmporab1w  6128  unielxp  6241  f1o2ndf1  6295  cnvoprab  6301  tfrlem1  6375  tfr1onlemaccex  6415  tfrcllemaccex  6428  ecopovtrn  6700  ecopovtrng  6703  findcard2d  6961  findcard2sd  6962  fidcenumlemr  7030  difinfsn  7175  nnnninfeq2  7204  ismkvnex  7230  cc3  7353  ltexnqi  7495  prcdnql  7570  prcunqu  7571  prnmaxl  7574  prnminu  7575  ltprordil  7675  1idprl  7676  1idpru  7677  ltexprlemm  7686  ltexprlemopu  7689  ltexprlemru  7698  recexgt0sr  7859  mulgt0sr  7864  ltrenn  7941  nnindnn  7979  nnind  9025  nnmulcl  9030  nnnegz  9348  supinfneg  9688  infsupneg  9689  ublbneg  9706  ixxssxr  9994  ixxssixx  9996  iccshftri  10089  iccshftli  10091  iccdili  10093  icccntri  10095  1fv  10233  fzo1fzo0n0  10278  elfzonlteqm1  10305  ssfzo12  10319  exbtwnzlemshrink  10357  flqeqceilz  10429  zmodidfzoimp  10465  modfzo0difsn  10506  frec2uzltd  10514  frec2uzrdg  10520  frecuzrdgg  10527  seq3clss  10582  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  seq3caopr3  10602  seqcaopr3g  10603  seq3f1olemp  10626  seqf1oglem2a  10629  seqf1og  10632  seq3id2  10637  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  ser3ge0  10647  exp3vallem  10651  modqexp  10777  fihashf1rn  10899  hashfzp1  10935  seq3coll  10953  cjre  11066  climeu  11480  climub  11528  fsum2d  11619  fsumabs  11649  fsumiun  11661  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  prodfap0  11729  prodfrecap  11730  ntrivcvgap  11732  fprodabs  11800  fprod2d  11807  dvdsmod0  11977  p1modz1  11978  dvdsmodexp  11979  dvdsabseq  12031  mulsucdiv2z  12069  nno  12090  nn0o  12091  dfgcd2  12208  lcmgcdlem  12272  cncongr2  12299  exprmfct  12333  eulerthlemrprm  12424  eulerthlema  12425  dvdsprmpweqnn  12532  dvdsprmpweqle  12533  pcmpt  12539  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemhom  12659  nninfdclemlt  12695  setsn0fun  12742  insubm  13189  ghmghmrn  13471  srgpcomp  13624  ringrng  13670  gsumfzfsumlemm  14221  tg2  14404  hmeof1o  14653  tgioo  14898  dvmptfsum  15069  plycolemc  15102  perfectlem2  15344  gausslemma2dlem0i  15406  lgsquad2lem2  15431  2lgslem3  15450  2lgs  15453  2lgsoddprm  15462  bdfind  15700  bj-nn0sucALT  15732  nninfsellemqall  15770