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  1882  ceqex  2904  sbcn1  3050  sbcim1  3051  sbcbi1  3052  sbcel21v  3067  ifnetruedc  3617  peano2  4650  sotri  5086  relcoi1  5222  f0rn0  5481  f1ocnv  5546  tz6.12c  5618  funbrfv  5629  fnbrfvb  5631  fvmptss2  5666  elfvmptrab1  5686  oprabid  5988  eloprabga  6044  elovmporab  6158  elovmporab1w  6159  unielxp  6272  f1o2ndf1  6326  cnvoprab  6332  tfrlem1  6406  tfr1onlemaccex  6446  tfrcllemaccex  6459  ecopovtrn  6731  ecopovtrng  6734  findcard2d  7002  findcard2sd  7003  fidcenumlemr  7071  difinfsn  7216  nnnninfeq2  7245  ismkvnex  7271  cc3  7395  ltexnqi  7537  prcdnql  7612  prcunqu  7613  prnmaxl  7616  prnminu  7617  ltprordil  7717  1idprl  7718  1idpru  7719  ltexprlemm  7728  ltexprlemopu  7731  ltexprlemru  7740  recexgt0sr  7901  mulgt0sr  7906  ltrenn  7983  nnindnn  8021  nnind  9067  nnmulcl  9072  nnnegz  9390  supinfneg  9731  infsupneg  9732  ublbneg  9749  ixxssxr  10037  ixxssixx  10039  iccshftri  10132  iccshftli  10134  iccdili  10136  icccntri  10138  1fv  10276  fzo1fzo0n0  10324  elfzonlteqm1  10356  ssfzo12  10370  exbtwnzlemshrink  10408  flqeqceilz  10480  zmodidfzoimp  10516  modfzo0difsn  10557  frec2uzltd  10565  frec2uzrdg  10571  frecuzrdgg  10578  seq3clss  10633  seq3fveq2  10637  seqfveq2g  10639  seq3shft2  10643  seqshft2g  10644  monoord  10647  seq3split  10650  seqsplitg  10651  seq3caopr3  10653  seqcaopr3g  10654  seq3f1olemp  10677  seqf1oglem2a  10680  seqf1og  10683  seq3id2  10688  seq3homo  10689  seq3z  10690  seqhomog  10692  seqfeq4g  10693  ser3ge0  10698  exp3vallem  10702  modqexp  10828  fihashf1rn  10950  hashfzp1  10986  seq3coll  11004  swrdswrd  11176  cjre  11263  climeu  11677  climub  11725  fsum2d  11816  fsumabs  11846  fsumiun  11858  cvgratnnlemnexp  11905  cvgratnnlemmn  11906  prodfap0  11926  prodfrecap  11927  ntrivcvgap  11929  fprodabs  11997  fprod2d  12004  dvdsmod0  12174  p1modz1  12175  dvdsmodexp  12176  dvdsabseq  12228  mulsucdiv2z  12266  nno  12287  nn0o  12288  dfgcd2  12405  lcmgcdlem  12469  cncongr2  12496  exprmfct  12530  eulerthlemrprm  12621  eulerthlema  12622  dvdsprmpweqnn  12729  dvdsprmpweqle  12730  pcmpt  12736  ennnfoneleminc  12852  ennnfonelemkh  12853  ennnfonelemhf1o  12854  ennnfonelemhom  12856  nninfdclemlt  12892  setsn0fun  12939  insubm  13387  ghmghmrn  13669  srgpcomp  13822  ringrng  13868  gsumfzfsumlemm  14419  tg2  14602  hmeof1o  14851  tgioo  15096  dvmptfsum  15267  plycolemc  15300  perfectlem2  15542  gausslemma2dlem0i  15604  lgsquad2lem2  15629  2lgslem3  15648  2lgs  15651  2lgsoddprm  15660  bdfind  16016  bj-nn0sucALT  16048  nninfsellemqall  16087