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  1907  ceqex  2946  sbcn1  3092  sbcim1  3093  sbcbi1  3094  sbcel21v  3109  ifnetruedc  3668  peano2  4719  sotri  5160  relcoi1  5296  f0rn0  5564  f1ocnv  5629  tz6.12c  5702  funbrfv  5715  fnbrfvb  5717  fvmptss2  5754  elfvmptrab1  5774  oprabid  6084  eloprabga  6142  elovmporab  6256  elovmporab1w  6257  relmptopab  6258  unielxp  6370  f1o2ndf1  6426  cnvoprab  6432  ressuppss  6456  tfrlem1  6541  tfr1onlemaccex  6581  tfrcllemaccex  6594  ecopovtrn  6868  ecopovtrng  6871  findcard2d  7150  findcard2sd  7151  fidcenumlemr  7227  fsuppimp  7247  difinfsn  7393  nnnninfeq2  7422  ismkvnex  7448  cc3  7587  ltexnqi  7729  prcdnql  7804  prcunqu  7805  prnmaxl  7808  prnminu  7809  ltprordil  7909  1idprl  7910  1idpru  7911  ltexprlemm  7920  ltexprlemopu  7923  ltexprlemru  7932  recexgt0sr  8093  mulgt0sr  8098  ltrenn  8175  nnindnn  8213  nnind  9258  nnmulcl  9263  nnnegz  9585  supinfneg  9933  infsupneg  9934  ublbneg  9951  ixxssxr  10239  ixxssixx  10241  iccshftri  10334  iccshftli  10336  iccdili  10338  icccntri  10340  1fv  10480  fzo1fzo0n0  10529  elfzonlteqm1  10562  ssfzo12  10576  exbtwnzlemshrink  10615  flqeqceilz  10687  zmodidfzoimp  10723  modfzo0difsn  10764  frec2uzltd  10772  frec2uzrdg  10778  frecuzrdgg  10785  seq3clss  10840  seq3fveq2  10844  seqfveq2g  10846  seq3shft2  10850  seqshft2g  10851  monoord  10854  seq3split  10857  seqsplitg  10858  seq3caopr3  10860  seqcaopr3g  10861  seq3f1olemp  10884  seqf1oglem2a  10887  seqf1og  10890  seq3id2  10895  seq3homo  10896  seq3z  10897  seqhomog  10899  seqfeq4g  10900  ser3ge0  10905  exp3vallem  10909  modqexp  11036  fihashf1rn  11159  hashfzp1  11197  seq3coll  11222  swrdswrd  11405  pfxccatin12lem2a  11427  pfxccatin12  11433  swrdccat  11435  pfxccat3a  11438  swrdccatin1d  11443  swrdccatin2d  11444  cjre  11575  climeu  11989  climub  12037  fsum2d  12129  fsumabs  12159  fsumiun  12171  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  prodfap0  12239  prodfrecap  12240  ntrivcvgap  12242  fprodabs  12310  fprod2d  12317  dvdsmod0  12487  p1modz1  12488  dvdsmodexp  12489  dvdsabseq  12541  mulsucdiv2z  12579  nno  12600  nn0o  12601  dfgcd2  12718  lcmgcdlem  12782  cncongr2  12809  exprmfct  12843  eulerthlemrprm  12934  eulerthlema  12935  dvdsprmpweqnn  13042  dvdsprmpweqle  13043  pcmpt  13049  ballotfilemfc0  13157  ennnfoneleminc  13183  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemhom  13187  nninfdclemlt  13223  setsn0fun  13270  insubm  13719  ghmghmrn  14001  srgpcomp  14155  ringrng  14201  gsumfzfsumlemm  14784  tg2  14974  hmeof1o  15223  tgioo  15468  dvmptfsum  15639  plycolemc  15672  perfectlem2  15917  gausslemma2dlem0i  15979  lgsquad2lem2  16004  2lgslem3  16023  2lgs  16026  2lgsoddprm  16035  umgrnloop  16160  usgredg2vlem2  16267  subgrprop  16303  wlkv  16370  wlkl1loop  16402  wlk1walkdom  16403  uspgr2wlkeqi  16411  wlkres  16423  umgrclwwlkge2  16446  clwwlknp  16461  clwwlkext2edg  16466  clwwlknun  16485  eupth2fi  16523  bdfind  16765  bj-nn0sucALT  16797  nninfsellemqall  16842