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  6782  oprabidw  7181  oprabid  7182  frxp  7814  smo11  7995  oaordex  8178  oaass  8181  omordi  8186  oeordsuc  8214  nnmordi  8251  nnmord  8252  nnaordex  8258  brecop  8384  findcard2  8752  elfiun  8888  ordiso2  8973  ordtypelem7  8982  cantnf  9150  coftr  9689  domtriomlem  9858  prlem936  10463  zindd  12077  supxrun  12703  ccatopth2  14073  cau3lem  14708  climcau  15021  dvdsabseq  15657  divalglem8  15745  lcmf  15971  dirtr  17840  frgpnabllem1  18987  dprddisj2  19155  znrrg  20706  opnnei  21722  restntr  21784  lpcls  21966  comppfsc  22134  ufilmax  22509  ufileu  22521  flimfnfcls  22630  alexsubALTlem4  22652  qustgplem  22723  metrest  23128  caubl  23905  ulmcau  24977  ulmcn  24981  usgr2wlkneq  27531  erclwwlksym  27793  erclwwlktr  27794  erclwwlknsym  27843  erclwwlkntr  27844  sumdmdlem  30189  bnj1280  32287  fundmpss  33004  dfon2lem8  33030  nodenselem8  33190  ifscgr  33500  btwnconn1lem11  33553  btwnconn2  33558  finminlem  33661  opnrebl2  33664  fvineqsneq  34687  poimirlem21  34907  poimirlem26  34912  filbcmb  35009  seqpo  35016  mpobi123f  35434  mptbi12f  35438  ac6s6  35444  dia2dimlem12  38205  ntrk0kbimka  40382  truniALT  40868  onfrALTlem3  40871  ee223  40961  paireqne  43666  fmtnofac2lem  43723  setrec1lem4  44786