MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpdd Structured version   Visualization version   GIF version

Theorem mpdd 43
Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 15. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpdd.1 (𝜑 → (𝜓𝜒))
mpdd.2 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mpdd (𝜑 → (𝜓𝜃))

Proof of Theorem mpdd
StepHypRef Expression
1 mpdd.1 . 2 (𝜑 → (𝜓𝜒))
2 mpdd.2 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32a2d 29 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
41, 3mpd 15 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  mpid  44  mpdi  45  syld  47  syl6c  70  mpteqb  6338  oprabid  6717  frxp  7332  smo11  7506  oaordex  7683  oaass  7686  omordi  7691  oeordsuc  7719  nnmordi  7756  nnmord  7757  nnaordex  7763  brecop  7883  findcard2  8241  elfiun  8377  ordiso2  8461  ordtypelem7  8470  cantnf  8628  coftr  9133  domtriomlem  9302  prlem936  9907  zindd  11516  supxrun  12184  ccatopth2  13517  cau3lem  14138  climcau  14445  dvdsabseq  15082  divalglem8  15170  lcmf  15393  dirtr  17283  frgpnabllem1  18322  dprddisj2  18484  znrrg  19962  opnnei  20972  restntr  21034  lpcls  21216  comppfsc  21383  ufilmax  21758  ufileu  21770  flimfnfcls  21879  alexsubALTlem4  21901  qustgplem  21971  metrest  22376  caubl  23152  ulmcau  24194  ulmcn  24198  usgr2wlkneq  26708  erclwwlksym  26978  erclwwlktr  26979  erclwwlknsym  27034  erclwwlkntr  27035  sumdmdlem  29405  bnj1280  31214  fundmpss  31790  dfon2lem8  31819  nodenselem8  31966  ifscgr  32276  btwnconn1lem11  32329  btwnconn2  32334  finminlem  32437  opnrebl2  32441  poimirlem21  33560  poimirlem26  33565  filbcmb  33665  seqpo  33673  mpt2bi123f  34101  mptbi12f  34105  ac6s6  34110  dia2dimlem12  36681  ntrk0kbimka  38654  truniALT  39068  onfrALTlem3  39076  ee223  39176  fmtnofac2lem  41805  setrec1lem4  42762
  Copyright terms: Public domain W3C validator