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  1738  equvel  2455  propeqop  5506  funopsn  7142  xpexr  7905  omordi  8562  omwordi  8567  odi  8575  omass  8576  oen0  8582  oewordi  8587  oewordri  8588  nnmwordi  8631  omabs  8646  fisupg  9287  fiinfg  9490  cantnfle  9662  cantnflem1  9680  pr2neOLD  9996  gchina  10690  nqereu  10920  supsrlem  11102  1re  11210  lemul1a  12064  xlemul1a  13263  xrsupsslem  13282  xrinfmsslem  13283  xrub  13287  supxrunb1  13294  supxrunb2  13295  difelfzle  13610  addmodlteq  13907  seqcl2  13982  facdiv  14243  facwordi  14245  faclbnd  14246  pfxccat3  14680  dvdsabseq  16252  divgcdcoprm0  16598  2mulprm  16626  exprmfct  16637  prmfac1  16654  pockthg  16835  cply1mul  21809  mdetralt  22101  cmpsub  22895  fbfinnfr  23336  alexsubALTlem2  23543  alexsubALTlem3  23544  ovolicc2lem3  25027  fta1g  25676  fta1  25812  mulcxp  26184  cxpcn3lem  26244  gausslemma2dlem4  26861  colinearalg  28157  upgrwlkdvdelem  28982  umgr2wlk  29192  clwwlknwwlksn  29280  clwwlknonex2lem2  29350  dmdbr5ati  31662  cvmlift3lem4  34301  dfon2lem9  34751  fscgr  35040  colinbtwnle  35078  broutsideof2  35082  gg-dvfsumlem2  35171  a1i14  35173  a1i24  35174  ordcmp  35320  bj-peircestab  35417  wl-aleq  36392  itg2addnc  36530  filbcmb  36596  mpobi123f  37018  mptbi12f  37022  ac6s6  37028  ltrnid  38994  cdleme25dN  39215  nn0rppwr  41219  ntrneiiso  42827  ee323  43254  vd13  43347  vd23  43348  ee03  43487  ee23an  43503  ee32  43505  ee32an  43507  ee123  43509  iccpartgt  46081  stgoldbwt  46430  tgoldbach  46471  nzerooringczr  46923