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 ⊢ (𝜓 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldan  282  ax16i  1911  ceqex  2953  sbcn1  3099  sbcim1  3100  sbcbi1  3101  sbcel21v  3116  ifnetruedc  3684  peano2  4744  sotri  5186  relcoi1  5322  f0rn0  5590  f1ocnv  5655  tz6.12c  5728  funbrfv  5742  fnbrfvb  5744  fvmptss2  5783  elfvmptrab1  5804  oprabid  6120  eloprabga  6178  elovmporab  6292  elovmporab1w  6293  relmptopab  6294  unielxp  6412  f1o2ndf1  6468  cnvoprab  6474  ressuppss  6498  tfrlem1  6583  tfr1onlemaccex  6623  tfrcllemaccex  6636  ecopovtrn  6910  ecopovtrng  6913  findcard2d  7200  findcard2sd  7201  fidcenumlemr  7278  fsuppimp  7298  difinfsn  7447  nnnninfeq2  7476  ismkvnex  7502  cc3  7641  ltexnqi  7783  prcdnql  7858  prcunqu  7859  prnmaxl  7862  prnminu  7863  ltprordil  7963  1idprl  7964  1idpru  7965  ltexprlemm  7974  ltexprlemopu  7977  ltexprlemru  7986  recexgt0sr  8147  mulgt0sr  8152  ltrenn  8229  nnindnn  8267  nnind  9330  nnmulcl  9335  nnnegz  9659  supinfneg  10012  infsupneg  10013  ublbneg  10030  ixxssxr  10320  ixxssixx  10322  iccshftri  10415  iccshftli  10417  iccdili  10419  icccntri  10421  1fv  10564  fzo1fzo0n0  10613  elfzonlteqm1  10646  ssfzo12  10660  exbtwnzlemshrink  10701  flqeqceilz  10777  zmodidfzoimp  10813  modfzo0difsn  10854  frec2uzltd  10862  frec2uzrdg  10868  frecuzrdgg  10875  seq3clss  10930  seq3fveq2  10934  seqfveq2g  10936  seq3shft2  10940  seqshft2g  10941  monoord  10944  seq3split  10947  seqsplitg  10948  seq3caopr3  10950  seqcaopr3g  10951  seq3f1olemp  10974  seqf1oglem2a  10977  seqf1og  10980  seq3id2  10985  seq3homo  10986  seq3z  10987  seqhomog  10989  seqfeq4g  10990  ser3ge0  10995  exp3vallem  10999  modqexp  11126  fihashf1rn  11250  hashfzp1  11288  seq3coll  11317  swrdswrd  11500  pfxccatin12lem2a  11522  pfxccatin12  11528  swrdccat  11530  pfxccat3a  11533  swrdccatin1d  11538  swrdccatin2d  11539  cjre  11670  climeu  12088  climub  12136  fsum2d  12228  fsumabs  12258  fsumiun  12270  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  prodfap0  12338  prodfrecap  12339  ntrivcvgap  12341  fprodabs  12409  fprod2d  12416  dvdsmod0  12586  p1modz1  12587  dvdsmodexp  12588  dvdsabseq  12640  mulsucdiv2z  12678  nno  12699  nn0o  12700  dfgcd2  12817  lcmgcdlem  12881  cncongr2  12908  exprmfct  12943  pwbdvdslemn  12970  eulerthlemrprm  13037  eulerthlema  13038  dvdsprmpweqnn  13145  dvdsprmpweqle  13146  pcmpt  13152  prmlem1a  13251  ballotfilemfc0  13291  ennnfoneleminc  13361  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemhom  13365  nninfdclemlt  13401  setsn0fun  13448  insubm  13852  ghmghmrn  14126  srgpcomp  14402  ringrng  14449  tg2  15298  hmeof1o  15547  tgioo  15792  dvmptfsum  15963  plycolemc  15996  perfectlem2  16312  bposlem5  16327  gausslemma2dlem0i  16393  lgsquad2lem2  16418  2lgslem3  16437  2lgs  16440  2lgsoddprm  16449  umgrnloop  16574  usgredg2vlem2  16681  subgrprop  16717  wlkv  16784  wlkl1loop  16816  wlk1walkdom  16817  uspgr2wlkeqi  16825  wlkres  16837  umgrclwwlkge2  16860  clwwlknp  16875  clwwlkext2edg  16880  clwwlknun  16899  eupth2fi  16937  bdfind  17189  bj-nn0sucALT  17221  nninfsellemqall  17276