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  1869  ceqex  2887  sbcn1  3033  sbcim1  3034  sbcbi1  3035  sbcel21v  3050  ifnetruedc  3598  peano2  4627  sotri  5061  relcoi1  5197  f0rn0  5448  f1ocnv  5513  tz6.12c  5584  funbrfv  5595  fnbrfvb  5597  fvmptss2  5632  elfvmptrab1  5652  oprabid  5950  eloprabga  6005  elovmporab  6118  elovmporab1w  6119  unielxp  6227  f1o2ndf1  6281  cnvoprab  6287  tfrlem1  6361  tfr1onlemaccex  6401  tfrcllemaccex  6414  ecopovtrn  6686  ecopovtrng  6689  findcard2d  6947  findcard2sd  6948  fidcenumlemr  7014  difinfsn  7159  nnnninfeq2  7188  ismkvnex  7214  cc3  7328  ltexnqi  7469  prcdnql  7544  prcunqu  7545  prnmaxl  7548  prnminu  7549  ltprordil  7649  1idprl  7650  1idpru  7651  ltexprlemm  7660  ltexprlemopu  7663  ltexprlemru  7672  recexgt0sr  7833  mulgt0sr  7838  ltrenn  7915  nnindnn  7953  nnind  8998  nnmulcl  9003  nnnegz  9320  supinfneg  9660  infsupneg  9661  ublbneg  9678  ixxssxr  9966  ixxssixx  9968  iccshftri  10061  iccshftli  10063  iccdili  10065  icccntri  10067  1fv  10205  fzo1fzo0n0  10250  elfzonlteqm1  10277  ssfzo12  10291  exbtwnzlemshrink  10317  flqeqceilz  10389  zmodidfzoimp  10425  modfzo0difsn  10466  frec2uzltd  10474  frec2uzrdg  10480  frecuzrdgg  10487  seq3clss  10542  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3f1olemp  10586  seqf1oglem2a  10589  seqf1og  10592  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  seqfeq4g  10602  ser3ge0  10607  exp3vallem  10611  modqexp  10737  fihashf1rn  10859  hashfzp1  10895  seq3coll  10913  cjre  11026  climeu  11439  climub  11487  fsum2d  11578  fsumabs  11608  fsumiun  11620  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  prodfap0  11688  prodfrecap  11689  ntrivcvgap  11691  fprodabs  11759  fprod2d  11766  dvdsmod0  11936  p1modz1  11937  dvdsmodexp  11938  dvdsabseq  11989  mulsucdiv2z  12026  nno  12047  nn0o  12048  dfgcd2  12151  lcmgcdlem  12215  cncongr2  12242  exprmfct  12276  eulerthlemrprm  12367  eulerthlema  12368  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  pcmpt  12481  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemhom  12572  nninfdclemlt  12608  setsn0fun  12655  insubm  13057  ghmghmrn  13333  srgpcomp  13486  ringrng  13532  gsumfzfsumlemm  14075  tg2  14228  hmeof1o  14477  tgioo  14714  gausslemma2dlem0i  15173  bdfind  15438  bj-nn0sucALT  15470  nninfsellemqall  15505