Theorem a1dd 50

Description: Double deduction introducing an antecedent. Deduction associated with a1d 25. Double deduction associated with ax-1 6 and a1i 11. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)

Hypothesis

Ref	Expression
a1dd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
a1dd	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

Proof of Theorem a1dd

Step	Hyp	Ref	Expression
1		a1dd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		ax-1 6	. 2 ⊢ (𝜒 → (𝜃 → 𝜒))
3	1, 2	syl6 35	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:  2a1dd  51  ad4ant13  1292  ad4ant124  1295  ad4ant23  1297  merco2  1661  equvel  2347  propeqop  4970  funopsn  6413  xpexr  7106  omordi  7646  omwordi  7651  odi  7659  omass  7660  oen0  7666  oewordi  7671  oewordri  7672  nnmwordi  7715  omabs  7727  fisupg  8208  fiinfg  8405  cantnfle  8568  cantnflem1  8586  pr2ne  8828  gchina  9521  nqereu  9751  supsrlem  9932  1re  10039  lemul1a  10877  nnsub  11059  xlemul1a  12118  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrunb1  12149  supxrunb2  12150  difelfzle  12452  addmodlteq  12745  seqcl2  12819  facdiv  13074  facwordi  13076  faclbnd  13077  swrdswrdlem  13459  swrdccat3  13492  dvdsabseq  15035  divgcdcoprm0  15379  exprmfct  15416  prmfac1  15431  pockthg  15610  cply1mul  19664  mdetralt  20414  cmpsub  21203  fbfinnfr  21645  alexsubALTlem2  21852  alexsubALTlem3  21853  ovolicc2lem3  23287  fta1g  23927  fta1  24063  mulcxp  24431  cxpcn3lem  24488  gausslemma2dlem4  25094  colinearalg  25790  upgrwlkdvdelem  26632  umgr2wlk  26845  clwwlksnwwlksn  27209  dmdbr5ati  29281  cvmlift3lem4  31304  dfon2lem9  31696  fscgr  32187  colinbtwnle  32225  broutsideof2  32229  a1i14  32294  a1i24  32295  ordcmp  32446  wl-aleq  33322  itg2addnc  33464  filbcmb  33535  mpt2bi123f  33971  mptbi12f  33975  ac6s6  33980  ltrnid  35421  cdleme25dN  35644  ntrneiiso  38389  ee323  38714  vd13  38826  vd23  38827  ee03  38968  ee23an  38984  ee32  38986  ee32an  38988  ee123  38990  iccpartgt  41363  pfxccat3  41426  stgoldbwt  41664  tgoldbach  41705  tgoldbachOLD  41712  nzerooringczr  42072