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  1884  ceqex  2910  sbcn1  3056  sbcim1  3057  sbcbi1  3058  sbcel21v  3073  ifnetruedc  3626  peano2  4664  sotri  5100  relcoi1  5236  f0rn0  5496  f1ocnv  5561  tz6.12c  5633  funbrfv  5644  fnbrfvb  5646  fvmptss2  5682  elfvmptrab1  5702  oprabid  6006  eloprabga  6062  elovmporab  6176  elovmporab1w  6177  unielxp  6290  f1o2ndf1  6344  cnvoprab  6350  tfrlem1  6424  tfr1onlemaccex  6464  tfrcllemaccex  6477  ecopovtrn  6749  ecopovtrng  6752  findcard2d  7021  findcard2sd  7022  fidcenumlemr  7090  difinfsn  7235  nnnninfeq2  7264  ismkvnex  7290  cc3  7422  ltexnqi  7564  prcdnql  7639  prcunqu  7640  prnmaxl  7643  prnminu  7644  ltprordil  7744  1idprl  7745  1idpru  7746  ltexprlemm  7755  ltexprlemopu  7758  ltexprlemru  7767  recexgt0sr  7928  mulgt0sr  7933  ltrenn  8010  nnindnn  8048  nnind  9094  nnmulcl  9099  nnnegz  9417  supinfneg  9758  infsupneg  9759  ublbneg  9776  ixxssxr  10064  ixxssixx  10066  iccshftri  10159  iccshftli  10161  iccdili  10163  icccntri  10165  1fv  10303  fzo1fzo0n0  10351  elfzonlteqm1  10383  ssfzo12  10397  exbtwnzlemshrink  10435  flqeqceilz  10507  zmodidfzoimp  10543  modfzo0difsn  10584  frec2uzltd  10592  frec2uzrdg  10598  frecuzrdgg  10605  seq3clss  10660  seq3fveq2  10664  seqfveq2g  10666  seq3shft2  10670  seqshft2g  10671  monoord  10674  seq3split  10677  seqsplitg  10678  seq3caopr3  10680  seqcaopr3g  10681  seq3f1olemp  10704  seqf1oglem2a  10707  seqf1og  10710  seq3id2  10715  seq3homo  10716  seq3z  10717  seqhomog  10719  seqfeq4g  10720  ser3ge0  10725  exp3vallem  10729  modqexp  10855  fihashf1rn  10977  hashfzp1  11013  seq3coll  11031  swrdswrd  11203  pfxccatin12lem2a  11225  pfxccatin12  11231  swrdccat  11233  pfxccat3a  11236  swrdccatin1d  11241  swrdccatin2d  11242  cjre  11359  climeu  11773  climub  11821  fsum2d  11912  fsumabs  11942  fsumiun  11954  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  prodfap0  12022  prodfrecap  12023  ntrivcvgap  12025  fprodabs  12093  fprod2d  12100  dvdsmod0  12270  p1modz1  12271  dvdsmodexp  12272  dvdsabseq  12324  mulsucdiv2z  12362  nno  12383  nn0o  12384  dfgcd2  12501  lcmgcdlem  12565  cncongr2  12592  exprmfct  12626  eulerthlemrprm  12717  eulerthlema  12718  dvdsprmpweqnn  12825  dvdsprmpweqle  12826  pcmpt  12832  ennnfoneleminc  12948  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemhom  12952  nninfdclemlt  12988  setsn0fun  13035  insubm  13484  ghmghmrn  13766  srgpcomp  13919  ringrng  13965  gsumfzfsumlemm  14516  tg2  14699  hmeof1o  14948  tgioo  15193  dvmptfsum  15364  plycolemc  15397  perfectlem2  15639  gausslemma2dlem0i  15701  lgsquad2lem2  15726  2lgslem3  15745  2lgs  15748  2lgsoddprm  15757  umgrnloop  15881  usgredg2vlem2  15986  bdfind  16219  bj-nn0sucALT  16251  nninfsellemqall  16292