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  6990  oprabidw  7422  oprabid  7423  frxp  8100  smo11  8329  oaordex  8521  oaass  8524  omordi  8529  oeordsuc  8558  nnmordi  8595  nnmord  8596  nnaordex  8602  brecop  8786  elfiun  9370  ordiso2  9457  ordtypelem7  9466  cantnf  9642  coftr  10224  domtriomlem  10393  prlem936  10999  zindd  12668  supxrun  13313  ccatopth2  14724  cau3lem  15373  climcau  15689  dvdsabseq  16338  divalglem8  16425  lcmf  16658  dirtr  18625  frgpnabllem1  19904  dprddisj2  20072  znrrg  21605  opnnei  23168  restntr  23230  lpcls  23412  comppfsc  23580  ufilmax  23955  ufileu  23967  flimfnfcls  24076  alexsubALTlem4  24098  qustgplem  24169  metrest  24572  caubl  25358  ulmcau  26446  ulmcn  26450  nodenselem8  27743  usgr2wlkneq  29913  erclwwlksym  30180  erclwwlktr  30181  erclwwlknsym  30229  erclwwlkntr  30230  sumdmdlem  32578  bnj1280  35276  antnestlaw2  36003  fundmpss  36078  dfon2lem8  36099  ifscgr  36355  btwnconn1lem11  36408  btwnconn2  36413  finminlem  36639  opnrebl2  36642  fvineqsneq  37867  poimirlem21  38101  poimirlem26  38106  filbcmb  38200  seqpo  38207  mpobi123f  38622  mptbi12f  38626  ac6s6  38632  dia2dimlem12  41660  aks6d1c1p2  42687  ntrk0kbimka  44576  truniALT  45078  onfrALTlem3  45081  ee223  45171  ormklocald  47411  paireqne  48078  fmtnofac2lem  48138  setrec1lem4  50272