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  6255  oprabid  6631  frxp  7232  smo11  7406  oaordex  7583  oaass  7586  omordi  7591  oeordsuc  7619  nnmordi  7656  nnmord  7657  nnaordex  7663  brecop  7785  findcard2  8144  elfiun  8280  ordiso2  8364  ordtypelem7  8373  cantnf  8534  coftr  9039  domtriomlem  9208  prlem936  9813  zindd  11422  supxrun  12089  ccatopth2  13409  cau3lem  14028  climcau  14335  dvdsabseq  14959  divalglem8  15047  lcmf  15270  dirtr  17157  frgpnabllem1  18197  dprddisj2  18359  znrrg  19833  opnnei  20834  restntr  20896  lpcls  21078  comppfsc  21245  ufilmax  21621  ufileu  21633  flimfnfcls  21742  alexsubALTlem4  21764  qustgplem  21834  metrest  22239  caubl  23014  ulmcau  24053  ulmcn  24057  usgr2wlkneq  26521  elwspths2on  26721  erclwwlkssym  26801  erclwwlkstr  26802  erclwwlksnsym  26813  erclwwlksntr  26814  sumdmdlem  29126  bnj1280  30796  fundmpss  31368  dfon2lem8  31396  nodenselem7  31550  nodenselem8  31551  ifscgr  31793  btwnconn1lem11  31846  btwnconn2  31851  finminlem  31954  opnrebl2  31958  poimirlem21  33062  poimirlem26  33067  filbcmb  33167  seqpo  33175  mpt2bi123f  33603  mptbi12f  33607  ac6s6  33612  dia2dimlem12  35844  ntrk0kbimka  37819  truniALT  38233  onfrALTlem3  38241  ee223  38341  fmtnofac2lem  40779  setrec1lem4  41730
 Copyright terms: Public domain W3C validator