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  2453  propeqop  5508  funopsn  7149  xpexr  7913  omordi  8570  omwordi  8575  odi  8583  omass  8584  oen0  8590  oewordi  8595  oewordri  8596  nnmwordi  8639  omabs  8654  fisupg  9295  fiinfg  9498  cantnfle  9670  cantnflem1  9688  pr2neOLD  10004  gchina  10698  nqereu  10928  supsrlem  11110  1re  11220  lemul1a  12074  xlemul1a  13273  xrsupsslem  13292  xrinfmsslem  13293  xrub  13297  supxrunb1  13304  supxrunb2  13305  difelfzle  13620  addmodlteq  13917  seqcl2  13992  facdiv  14253  facwordi  14255  faclbnd  14256  pfxccat3  14690  dvdsabseq  16262  divgcdcoprm0  16608  2mulprm  16636  exprmfct  16647  prmfac1  16664  pockthg  16845  cply1mul  22040  mdetralt  22332  cmpsub  23126  fbfinnfr  23567  alexsubALTlem2  23774  alexsubALTlem3  23775  ovolicc2lem3  25270  fta1g  25919  fta1  26055  mulcxp  26427  cxpcn3lem  26489  gausslemma2dlem4  27106  colinearalg  28433  upgrwlkdvdelem  29258  umgr2wlk  29468  clwwlknwwlksn  29556  clwwlknonex2lem2  29626  dmdbr5ati  31940  cvmlift3lem4  34609  dfon2lem9  35065  fscgr  35354  colinbtwnle  35392  broutsideof2  35396  gg-dvfsumlem2  35471  a1i14  35490  a1i24  35491  ordcmp  35637  bj-peircestab  35734  wl-aleq  36709  itg2addnc  36847  filbcmb  36913  mpobi123f  37335  mptbi12f  37339  ac6s6  37345  ltrnid  39311  cdleme25dN  39532  nn0rppwr  41528  ntrneiiso  43146  ee323  43573  vd13  43666  vd23  43667  ee03  43806  ee23an  43822  ee32  43824  ee32an  43826  ee123  43828  iccpartgt  46395  stgoldbwt  46744  tgoldbach  46785  nzerooringczr  47060