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  6953  oprabidw  7384  oprabid  7385  frxp  8066  smo11  8294  oaordex  8483  oaass  8486  omordi  8491  oeordsuc  8519  nnmordi  8556  nnmord  8557  nnaordex  8563  brecop  8744  elfiun  9339  ordiso2  9426  ordtypelem7  9435  cantnf  9608  coftr  10186  domtriomlem  10355  prlem936  10960  zindd  12596  supxrun  13237  ccatopth2  14642  cau3lem  15281  climcau  15597  dvdsabseq  16243  divalglem8  16330  lcmf  16563  dirtr  18527  frgpnabllem1  19771  dprddisj2  19939  znrrg  21491  opnnei  23024  restntr  23086  lpcls  23268  comppfsc  23436  ufilmax  23811  ufileu  23823  flimfnfcls  23932  alexsubALTlem4  23954  qustgplem  24025  metrest  24429  caubl  25225  ulmcau  26321  ulmcn  26325  nodenselem8  27620  usgr2wlkneq  29720  erclwwlksym  29984  erclwwlktr  29985  erclwwlknsym  30033  erclwwlkntr  30034  sumdmdlem  32381  bnj1280  35006  antnestlaw2  35684  fundmpss  35759  dfon2lem8  35783  ifscgr  36037  btwnconn1lem11  36090  btwnconn2  36095  finminlem  36311  opnrebl2  36314  fvineqsneq  37405  poimirlem21  37640  poimirlem26  37645  filbcmb  37739  seqpo  37746  mpobi123f  38161  mptbi12f  38165  ac6s6  38171  dia2dimlem12  41074  aks6d1c1p2  42102  ntrk0kbimka  44032  truniALT  44535  onfrALTlem3  44538  ee223  44628  ormklocald  46875  paireqne  47515  fmtnofac2lem  47572  setrec1lem4  49695