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  1739  equvel  2456  propeqop  5506  funopsn  7141  xpexr  7904  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  21800  mdetralt  22092  cmpsub  22886  fbfinnfr  23327  alexsubALTlem2  23534  alexsubALTlem3  23535  ovolicc2lem3  25018  fta1g  25667  fta1  25803  mulcxp  26175  cxpcn3lem  26235  gausslemma2dlem4  26852  colinearalg  28148  upgrwlkdvdelem  28973  umgr2wlk  29183  clwwlknwwlksn  29271  clwwlknonex2lem2  29341  dmdbr5ati  31653  cvmlift3lem4  34251  dfon2lem9  34701  fscgr  34990  colinbtwnle  35028  broutsideof2  35032  gg-dvfsumlem2  35121  a1i14  35123  a1i24  35124  ordcmp  35270  bj-peircestab  35367  wl-aleq  36342  itg2addnc  36480  filbcmb  36546  mpobi123f  36968  mptbi12f  36972  ac6s6  36978  ltrnid  38944  cdleme25dN  39165  nn0rppwr  41167  ntrneiiso  42775  ee323  43202  vd13  43295  vd23  43296  ee03  43435  ee23an  43451  ee32  43453  ee32an  43455  ee123  43457  iccpartgt  46030  stgoldbwt  46379  tgoldbach  46420  nzerooringczr  46872