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  2947  sbcn1  3093  sbcim1  3094  sbcbi1  3095  sbcel21v  3110  ifnetruedc  3670  peano2  4722  sotri  5163  relcoi1  5299  f0rn0  5567  f1ocnv  5632  tz6.12c  5705  funbrfv  5718  fnbrfvb  5720  fvmptss2  5757  elfvmptrab1  5777  oprabid  6090  eloprabga  6148  elovmporab  6262  elovmporab1w  6263  relmptopab  6264  unielxp  6381  f1o2ndf1  6437  cnvoprab  6443  ressuppss  6467  tfrlem1  6552  tfr1onlemaccex  6592  tfrcllemaccex  6605  ecopovtrn  6879  ecopovtrng  6882  findcard2d  7161  findcard2sd  7162  fidcenumlemr  7238  fsuppimp  7258  difinfsn  7404  nnnninfeq2  7433  ismkvnex  7459  cc3  7598  ltexnqi  7740  prcdnql  7815  prcunqu  7816  prnmaxl  7819  prnminu  7820  ltprordil  7920  1idprl  7921  1idpru  7922  ltexprlemm  7931  ltexprlemopu  7934  ltexprlemru  7943  recexgt0sr  8104  mulgt0sr  8109  ltrenn  8186  nnindnn  8224  nnind  9273  nnmulcl  9278  nnnegz  9600  supinfneg  9948  infsupneg  9949  ublbneg  9966  ixxssxr  10255  ixxssixx  10257  iccshftri  10350  iccshftli  10352  iccdili  10354  icccntri  10356  1fv  10498  fzo1fzo0n0  10547  elfzonlteqm1  10580  ssfzo12  10594  exbtwnzlemshrink  10635  flqeqceilz  10707  zmodidfzoimp  10743  modfzo0difsn  10784  frec2uzltd  10792  frec2uzrdg  10798  frecuzrdgg  10805  seq3clss  10860  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seqcaopr3g  10881  seq3f1olemp  10904  seqf1oglem2a  10907  seqf1og  10910  seq3id2  10915  seq3homo  10916  seq3z  10917  seqhomog  10919  seqfeq4g  10920  ser3ge0  10925  exp3vallem  10929  modqexp  11056  fihashf1rn  11179  hashfzp1  11217  seq3coll  11242  swrdswrd  11425  pfxccatin12lem2a  11447  pfxccatin12  11453  swrdccat  11455  pfxccat3a  11458  swrdccatin1d  11463  swrdccatin2d  11464  cjre  11595  climeu  12009  climub  12057  fsum2d  12149  fsumabs  12179  fsumiun  12191  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  prodfap0  12259  prodfrecap  12260  ntrivcvgap  12262  fprodabs  12330  fprod2d  12337  dvdsmod0  12507  p1modz1  12508  dvdsmodexp  12509  dvdsabseq  12561  mulsucdiv2z  12599  nno  12620  nn0o  12621  dfgcd2  12738  lcmgcdlem  12802  cncongr2  12829  exprmfct  12863  eulerthlemrprm  12954  eulerthlema  12955  dvdsprmpweqnn  13062  dvdsprmpweqle  13063  pcmpt  13069  ballotfilemfc0  13179  ennnfoneleminc  13249  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemhom  13253  nninfdclemlt  13289  setsn0fun  13336  insubm  13743  ghmghmrn  14019  srgpcomp  14236  ringrng  14282  gsumfzfsumlemm  14864  tg2  15054  hmeof1o  15303  tgioo  15548  dvmptfsum  15719  plycolemc  15752  perfectlem2  15997  gausslemma2dlem0i  16059  lgsquad2lem2  16084  2lgslem3  16103  2lgs  16106  2lgsoddprm  16115  umgrnloop  16240  usgredg2vlem2  16347  subgrprop  16383  wlkv  16450  wlkl1loop  16482  wlk1walkdom  16483  uspgr2wlkeqi  16491  wlkres  16503  umgrclwwlkge2  16526  clwwlknp  16541  clwwlkext2edg  16546  clwwlknun  16565  eupth2fi  16603  bdfind  16855  bj-nn0sucALT  16887  nninfsellemqall  16932