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  21422  cply1mul  22216  mdetralt  22528  cmpsub  23320  fbfinnfr  23761  alexsubALTlem2  23968  alexsubALTlem3  23969  ovolicc2lem3  25453  dvfsumlem2  25966  fta1g  26108  fta1  26249  taylply2  26308  mulcxp  26627  cxpcn3lem  26690  gausslemma2dlem4  27313  colinearalg  28890  upgrwlkdvdelem  29716  umgr2wlk  29929  clwwlknwwlksn  30017  clwwlknonex2lem2  30087  dmdbr5ati  32401  cvmlift3lem4  35302  antnestlaw2  35672  dfon2lem9  35772  fscgr  36061  colinbtwnle  36099  broutsideof2  36103  a1i14  36281  a1i24  36282  ordcmp  36428  bj-peircestab  36534  wl-aleq  37516  itg2addnc  37661  filbcmb  37727  mpobi123f  38149  mptbi12f  38153  ac6s6  38159  ltrnid  40122  cdleme25dN  40343  ntrneiiso  44073  ee323  44491  vd13  44584  vd23  44585  ee03  44723  ee23an  44739  ee32  44741  ee32an  44743  ee123  44745  iccpartgt  47421  stgoldbwt  47770  tgoldbach  47811  gpgedg2iv  48051