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  7011  oprabidw  7449  oprabid  7450  frxp  8136  smo11  8365  oaordex  8559  oaass  8562  omordi  8567  oeordsuc  8596  nnmordi  8633  nnmord  8634  nnaordex  8640  brecop  8824  elfiun  9415  ordiso2  9502  ordtypelem7  9511  cantnf  9687  setrec1lem4  9964  coftr  10344  domtriomlem  10513  prlem936  11125  zindd  12793  supxrun  13439  ccatopth2  14859  cau3lem  15515  climcau  15831  dvdsabseq  16476  divalglem8  16563  lcmf  16801  dirtr  18769  frgpnabllem1  20080  dprddisj2  20248  znrrg  21864  opnnei  23431  restntr  23493  lpcls  23675  comppfsc  23844  ufilmax  24219  ufileu  24231  flimfnfcls  24340  alexsubALTlem4  24362  qustgplem  24433  metrest  24836  caubl  25622  ulmcau  26715  ulmcn  26719  nodenselem8  28041  usgr2wlkneq  30335  erclwwlksym  30605  erclwwlktr  30606  erclwwlknsym  30654  erclwwlkntr  30655  sumdmdlem  33013  bnj1280  35643  antnestlaw2  36436  fundmpss  36511  dfon2lem8  36532  ifscgr  36789  btwnconn1lem11  36842  btwnconn2  36847  finminlem  37086  opnrebl2  37089  fvineqsneq  38315  poimirlem21  38539  poimirlem26  38544  filbcmb  38654  seqpo  38661  mpobi123f  39074  mptbi12f  39078  ac6s6  39084  dia2dimlem12  42112  aks6d1c1p2  43139  ntrk0kbimka  45024  truniALT  45509  onfrALTlem3  45512  ee223  45602  ormklocald  47855  paireqne  48562  fmtnofac2lem  48622