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  2461  propeqop  5487  funopsn  7143  xpexr  7919  resf1extb  7935  omordi  8583  omwordi  8588  odi  8596  omass  8597  oen0  8603  oewordi  8608  oewordri  8609  nnmwordi  8652  omabs  8668  fisupg  9301  fiinfg  9518  cantnfle  9690  cantnflem1  9708  pr2neOLD  10024  gchina  10718  nqereu  10948  supsrlem  11130  1re  11240  lemul1a  12100  xlemul1a  13309  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  supxrunb1  13340  supxrunb2  13341  difelfzle  13663  addmodlteq  13969  seqcl2  14043  facdiv  14310  facwordi  14312  faclbnd  14313  pfxccat3  14757  dvdsabseq  16337  nn0rppwr  16585  divgcdcoprm0  16689  2mulprm  16717  exprmfct  16728  prmfac1  16744  pockthg  16931  nzerooringczr  21446  cply1mul  22239  mdetralt  22551  cmpsub  23343  fbfinnfr  23784  alexsubALTlem2  23991  alexsubALTlem3  23992  ovolicc2lem3  25477  dvfsumlem2  25990  fta1g  26132  fta1  26273  taylply2  26332  mulcxp  26651  cxpcn3lem  26714  gausslemma2dlem4  27337  colinearalg  28894  upgrwlkdvdelem  29723  umgr2wlk  29936  clwwlknwwlksn  30024  clwwlknonex2lem2  30094  dmdbr5ati  32408  cvmlift3lem4  35349  dfon2lem9  35814  fscgr  36103  colinbtwnle  36141  broutsideof2  36145  a1i14  36323  a1i24  36324  ordcmp  36470  bj-peircestab  36576  wl-aleq  37558  itg2addnc  37703  filbcmb  37769  mpobi123f  38191  mptbi12f  38195  ac6s6  38201  ltrnid  40159  cdleme25dN  40380  ntrneiiso  44082  ee323  44500  vd13  44593  vd23  44594  ee03  44732  ee23an  44748  ee32  44750  ee32an  44752  ee123  44754  iccpartgt  47408  stgoldbwt  47757  tgoldbach  47798