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  7050  oprabidw  7481  oprabid  7482  frxp  8169  smo11  8422  oaordex  8616  oaass  8619  omordi  8624  oeordsuc  8652  nnmordi  8689  nnmord  8690  nnaordex  8696  brecop  8870  elfiun  9501  ordiso2  9586  ordtypelem7  9595  cantnf  9764  coftr  10344  domtriomlem  10513  prlem936  11118  zindd  12746  supxrun  13380  ccatopth2  14767  cau3lem  15405  climcau  15721  dvdsabseq  16363  divalglem8  16450  lcmf  16682  dirtr  18674  frgpnabllem1  19917  dprddisj2  20085  znrrg  21609  opnnei  23151  restntr  23213  lpcls  23395  comppfsc  23563  ufilmax  23938  ufileu  23950  flimfnfcls  24059  alexsubALTlem4  24081  qustgplem  24152  metrest  24560  caubl  25363  ulmcau  26458  ulmcn  26462  nodenselem8  27756  usgr2wlkneq  29794  erclwwlksym  30055  erclwwlktr  30056  erclwwlknsym  30104  erclwwlkntr  30105  sumdmdlem  32452  bnj1280  34998  fundmpss  35732  dfon2lem8  35756  ifscgr  36010  btwnconn1lem11  36063  btwnconn2  36068  finminlem  36286  opnrebl2  36289  fvineqsneq  37380  poimirlem21  37603  poimirlem26  37608  filbcmb  37702  seqpo  37709  mpobi123f  38124  mptbi12f  38128  ac6s6  38134  dia2dimlem12  41034  aks6d1c1p2  42068  ntrk0kbimka  44003  truniALT  44514  onfrALTlem3  44517  ee223  44607  paireqne  47387  fmtnofac2lem  47444  setrec1lem4  48788
  Copyright terms: Public domain W3C validator