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  7042  oprabidw  7469  oprabid  7470  frxp  8159  smo11  8412  oaordex  8604  oaass  8607  omordi  8612  oeordsuc  8640  nnmordi  8677  nnmord  8678  nnaordex  8684  brecop  8858  elfiun  9477  ordiso2  9562  ordtypelem7  9571  cantnf  9740  coftr  10320  domtriomlem  10489  prlem936  11094  zindd  12726  supxrun  13364  ccatopth2  14761  cau3lem  15399  climcau  15713  dvdsabseq  16356  divalglem8  16443  lcmf  16676  dirtr  18669  frgpnabllem1  19915  dprddisj2  20083  znrrg  21611  opnnei  23153  restntr  23215  lpcls  23397  comppfsc  23565  ufilmax  23940  ufileu  23952  flimfnfcls  24061  alexsubALTlem4  24083  qustgplem  24154  metrest  24562  caubl  25367  ulmcau  26464  ulmcn  26468  nodenselem8  27762  usgr2wlkneq  29802  erclwwlksym  30066  erclwwlktr  30067  erclwwlknsym  30115  erclwwlkntr  30116  sumdmdlem  32463  bnj1280  35027  fundmpss  35761  dfon2lem8  35785  ifscgr  36039  btwnconn1lem11  36092  btwnconn2  36097  finminlem  36313  opnrebl2  36316  fvineqsneq  37407  poimirlem21  37640  poimirlem26  37645  filbcmb  37739  seqpo  37746  mpobi123f  38161  mptbi12f  38165  ac6s6  38171  dia2dimlem12  41070  aks6d1c1p2  42103  ntrk0kbimka  44043  truniALT  44552  onfrALTlem3  44555  ee223  44645  paireqne  47462  fmtnofac2lem  47519  setrec1lem4  49044