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  2901  sbcn1  3047  sbcim1  3048  sbcbi1  3049  sbcel21v  3064  ifnetruedc  3614  peano2  4647  sotri  5083  relcoi1  5219  f0rn0  5477  f1ocnv  5542  tz6.12c  5613  funbrfv  5624  fnbrfvb  5626  fvmptss2  5661  elfvmptrab1  5681  oprabid  5983  eloprabga  6039  elovmporab  6153  elovmporab1w  6154  unielxp  6267  f1o2ndf1  6321  cnvoprab  6327  tfrlem1  6401  tfr1onlemaccex  6441  tfrcllemaccex  6454  ecopovtrn  6726  ecopovtrng  6729  findcard2d  6995  findcard2sd  6996  fidcenumlemr  7064  difinfsn  7209  nnnninfeq2  7238  ismkvnex  7264  cc3  7387  ltexnqi  7529  prcdnql  7604  prcunqu  7605  prnmaxl  7608  prnminu  7609  ltprordil  7709  1idprl  7710  1idpru  7711  ltexprlemm  7720  ltexprlemopu  7723  ltexprlemru  7732  recexgt0sr  7893  mulgt0sr  7898  ltrenn  7975  nnindnn  8013  nnind  9059  nnmulcl  9064  nnnegz  9382  supinfneg  9723  infsupneg  9724  ublbneg  9741  ixxssxr  10029  ixxssixx  10031  iccshftri  10124  iccshftli  10126  iccdili  10128  icccntri  10130  1fv  10268  fzo1fzo0n0  10314  elfzonlteqm1  10346  ssfzo12  10360  exbtwnzlemshrink  10398  flqeqceilz  10470  zmodidfzoimp  10506  modfzo0difsn  10547  frec2uzltd  10555  frec2uzrdg  10561  frecuzrdgg  10568  seq3clss  10623  seq3fveq2  10627  seqfveq2g  10629  seq3shft2  10633  seqshft2g  10634  monoord  10637  seq3split  10640  seqsplitg  10641  seq3caopr3  10643  seqcaopr3g  10644  seq3f1olemp  10667  seqf1oglem2a  10670  seqf1og  10673  seq3id2  10678  seq3homo  10679  seq3z  10680  seqhomog  10682  seqfeq4g  10683  ser3ge0  10688  exp3vallem  10692  modqexp  10818  fihashf1rn  10940  hashfzp1  10976  seq3coll  10994  swrdswrd  11164  cjre  11237  climeu  11651  climub  11699  fsum2d  11790  fsumabs  11820  fsumiun  11832  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  prodfap0  11900  prodfrecap  11901  ntrivcvgap  11903  fprodabs  11971  fprod2d  11978  dvdsmod0  12148  p1modz1  12149  dvdsmodexp  12150  dvdsabseq  12202  mulsucdiv2z  12240  nno  12261  nn0o  12262  dfgcd2  12379  lcmgcdlem  12443  cncongr2  12470  exprmfct  12504  eulerthlemrprm  12595  eulerthlema  12596  dvdsprmpweqnn  12703  dvdsprmpweqle  12704  pcmpt  12710  ennnfoneleminc  12826  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemhom  12830  nninfdclemlt  12866  setsn0fun  12913  insubm  13361  ghmghmrn  13643  srgpcomp  13796  ringrng  13842  gsumfzfsumlemm  14393  tg2  14576  hmeof1o  14825  tgioo  15070  dvmptfsum  15241  plycolemc  15274  perfectlem2  15516  gausslemma2dlem0i  15578  lgsquad2lem2  15603  2lgslem3  15622  2lgs  15625  2lgsoddprm  15634  bdfind  15956  bj-nn0sucALT  15988  nninfsellemqall  16026