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  6520  oprabid  6905  frxp  7521  smo11  7697  oaordex  7875  oaass  7878  omordi  7883  oeordsuc  7911  nnmordi  7948  nnmord  7949  nnaordex  7955  brecop  8075  findcard2  8439  elfiun  8575  ordiso2  8659  ordtypelem7  8668  cantnf  8837  coftr  9380  domtriomlem  9549  prlem936  10154  zindd  11744  supxrun  12364  ccatopth2  13695  cau3lem  14317  climcau  14624  dvdsabseq  15258  divalglem8  15343  lcmf  15565  dirtr  17441  frgpnabllem1  18477  dprddisj2  18640  znrrg  20121  opnnei  21138  restntr  21200  lpcls  21382  comppfsc  21549  ufilmax  21924  ufileu  21936  flimfnfcls  22045  alexsubALTlem4  22067  qustgplem  22137  metrest  22542  caubl  23318  ulmcau  24363  ulmcn  24367  usgr2wlkneq  26880  erclwwlksym  27164  erclwwlktr  27165  erclwwlknsym  27221  erclwwlkntr  27222  sumdmdlem  29605  bnj1280  31411  fundmpss  31986  dfon2lem8  32015  nodenselem8  32162  ifscgr  32472  btwnconn1lem11  32525  btwnconn2  32530  finminlem  32633  opnrebl2  32637  poimirlem21  33743  poimirlem26  33748  filbcmb  33847  seqpo  33854  mpt2bi123f  34281  mptbi12f  34285  ac6s6  34290  dia2dimlem12  36856  ntrk0kbimka  38837  truniALT  39249  onfrALTlem3  39257  ee223  39357  fmtnofac2lem  42055  setrec1lem4  43005
  Copyright terms: Public domain W3C validator