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  1736  equvel  2454  propeqop  5462  funopsn  7102  xpexr  7874  resf1extb  7890  omordi  8507  omwordi  8512  odi  8520  omass  8521  oen0  8527  oewordi  8532  oewordri  8533  nnmwordi  8576  omabs  8592  fisupg  9211  fiinfg  9428  cantnfle  9600  cantnflem1  9618  pr2neOLD  9934  gchina  10628  nqereu  10858  supsrlem  11040  1re  11150  lemul1a  12012  xlemul1a  13224  xrsupsslem  13243  xrinfmsslem  13244  xrub  13248  supxrunb1  13255  supxrunb2  13256  difelfzle  13578  addmodlteq  13887  seqcl2  13961  facdiv  14228  facwordi  14230  faclbnd  14231  pfxccat3  14675  dvdsabseq  16259  nn0rppwr  16507  divgcdcoprm0  16611  2mulprm  16639  exprmfct  16650  prmfac1  16666  pockthg  16853  nzerooringczr  21366  cply1mul  22159  mdetralt  22471  cmpsub  23263  fbfinnfr  23704  alexsubALTlem2  23911  alexsubALTlem3  23912  ovolicc2lem3  25396  dvfsumlem2  25909  fta1g  26051  fta1  26192  taylply2  26251  mulcxp  26570  cxpcn3lem  26633  gausslemma2dlem4  27256  colinearalg  28813  upgrwlkdvdelem  29639  umgr2wlk  29852  clwwlknwwlksn  29940  clwwlknonex2lem2  30010  dmdbr5ati  32324  cvmlift3lem4  35282  antnestlaw2  35652  dfon2lem9  35752  fscgr  36041  colinbtwnle  36079  broutsideof2  36083  a1i14  36261  a1i24  36262  ordcmp  36408  bj-peircestab  36514  wl-aleq  37496  itg2addnc  37641  filbcmb  37707  mpobi123f  38129  mptbi12f  38133  ac6s6  38139  ltrnid  40102  cdleme25dN  40323  ntrneiiso  44053  ee323  44471  vd13  44564  vd23  44565  ee03  44703  ee23an  44719  ee32  44721  ee32an  44723  ee123  44725  iccpartgt  47401  stgoldbwt  47750  tgoldbach  47791  gpgedg2iv  48031