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  merco2  1734  equvel  2464  propeqop  5526  funopsn  7182  xpexr  7958  omordi  8622  omwordi  8627  odi  8635  omass  8636  oen0  8642  oewordi  8647  oewordri  8648  nnmwordi  8691  omabs  8707  fisupg  9352  fiinfg  9568  cantnfle  9740  cantnflem1  9758  pr2neOLD  10074  gchina  10768  nqereu  10998  supsrlem  11180  1re  11290  lemul1a  12148  xlemul1a  13350  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  supxrunb1  13381  supxrunb2  13382  difelfzle  13698  addmodlteq  13997  seqcl2  14071  facdiv  14336  facwordi  14338  faclbnd  14339  pfxccat3  14782  dvdsabseq  16361  nn0rppwr  16608  divgcdcoprm0  16712  2mulprm  16740  exprmfct  16751  prmfac1  16767  pockthg  16953  nzerooringczr  21514  cply1mul  22321  mdetralt  22635  cmpsub  23429  fbfinnfr  23870  alexsubALTlem2  24077  alexsubALTlem3  24078  ovolicc2lem3  25573  dvfsumlem2  26087  fta1g  26229  fta1  26368  taylply2  26427  mulcxp  26745  cxpcn3lem  26808  gausslemma2dlem4  27431  colinearalg  28943  upgrwlkdvdelem  29772  umgr2wlk  29982  clwwlknwwlksn  30070  clwwlknonex2lem2  30140  dmdbr5ati  32454  cvmlift3lem4  35290  dfon2lem9  35755  fscgr  36044  colinbtwnle  36082  broutsideof2  36086  a1i14  36266  a1i24  36267  ordcmp  36413  bj-peircestab  36519  wl-aleq  37489  itg2addnc  37634  filbcmb  37700  mpobi123f  38122  mptbi12f  38126  ac6s6  38132  ltrnid  40092  cdleme25dN  40313  ntrneiiso  44053  ee323  44479  vd13  44572  vd23  44573  ee03  44712  ee23an  44728  ee32  44730  ee32an  44732  ee123  44734  iccpartgt  47301  stgoldbwt  47650  tgoldbach  47691