Theorem mpdd 44

Description: A nested modus ponens deduction. Double deduction associated with ax-mp 5. Deduction associated with mpd 16. (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 30	. 2 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
4	1, 3	mpd 16	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpid  45  mpdi  46  syld  48  syl6c  71  mpteqb  7014  oprabidw  7452  oprabid  7453  frxp  8141  smo11  8376  oaordex  8570  oaass  8573  omordi  8578  oeordsuc  8607  nnmordi  8644  nnmord  8645  nnaordex  8651  brecop  8835  elfiun  9426  ordiso2  9513  ordtypelem7  9522  cantnf  9698  setrec1lem4  9975  coftr  10355  domtriomlem  10524  prlem936  11136  zindd  12804  supxrun  13450  ccatopth2  14871  cau3lem  15528  climcau  15844  dvdsabseq  16489  divalglem8  16576  lcmf  16814  dirtr  18782  frgpnabllem1  20093  dprddisj2  20261  znrrg  21877  opnnei  23444  restntr  23506  lpcls  23688  comppfsc  23857  ufilmax  24232  ufileu  24244  flimfnfcls  24353  alexsubALTlem4  24375  qustgplem  24446  metrest  24849  caubl  25635  ulmcau  26728  ulmcn  26732  nodenselem8  28054  usgr2wlkneq  30348  erclwwlksym  30618  erclwwlktr  30619  erclwwlknsym  30667  erclwwlkntr  30668  sumdmdlem  33026  bnj1280  35697  antnestlaw2  36544  fundmpss  36625  dfon2lem8  36645  ifscgr  36902  btwnconn1lem11  36955  btwnconn2  36960  finminlem  37199  opnrebl2  37202  fvineqsneq  38429  poimirlem21  38653  poimirlem26  38658  filbcmb  38768  seqpo  38775  mpobi123f  39188  mptbi12f  39192  ac6s6  39198  dia2dimlem12  42226  aks6d1c1p2  43253  ntrk0kbimka  45133  truniALT  45618  onfrALTlem3  45621  ee223  45711  cocanss2  46016  ormklocald  47980  paireqne  48687  fmtnofac2lem  48747