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

Step	Hyp	Ref	Expression
1		mpdd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mpdd.2	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	a2d 29	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpd 15	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:  mpid  44  mpdi  45  syld  47  syl6c  70  mpteqb  6960  oprabidw  7389  oprabid  7390  frxp  8068  smo11  8296  oaordex  8485  oaass  8488  omordi  8493  oeordsuc  8522  nnmordi  8559  nnmord  8560  nnaordex  8566  brecop  8747  elfiun  9333  ordiso2  9420  ordtypelem7  9429  cantnf  9602  coftr  10183  domtriomlem  10352  prlem936  10958  zindd  12593  supxrun  13231  ccatopth2  14640  cau3lem  15278  climcau  15594  dvdsabseq  16240  divalglem8  16327  lcmf  16560  dirtr  18525  frgpnabllem1  19802  dprddisj2  19970  znrrg  21520  opnnei  23064  restntr  23126  lpcls  23308  comppfsc  23476  ufilmax  23851  ufileu  23863  flimfnfcls  23972  alexsubALTlem4  23994  qustgplem  24065  metrest  24468  caubl  25264  ulmcau  26360  ulmcn  26364  nodenselem8  27659  usgr2wlkneq  29829  erclwwlksym  30096  erclwwlktr  30097  erclwwlknsym  30145  erclwwlkntr  30146  sumdmdlem  32493  bnj1280  35176  antnestlaw2  35886  fundmpss  35961  dfon2lem8  35982  ifscgr  36238  btwnconn1lem11  36291  btwnconn2  36296  finminlem  36512  opnrebl2  36515  fvineqsneq  37617  poimirlem21  37842  poimirlem26  37847  filbcmb  37941  seqpo  37948  mpobi123f  38363  mptbi12f  38367  ac6s6  38373  dia2dimlem12  41335  aks6d1c1p2  42363  ntrk0kbimka  44280  truniALT  44782  onfrALTlem3  44785  ee223  44875  ormklocald  47118  paireqne  47757  fmtnofac2lem  47814  setrec1lem4  49935