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  1733  equvel  2475  propeqop  5390  funopsn  6905  xpexr  7617  omordi  8186  omwordi  8191  odi  8199  omass  8200  oen0  8206  oewordi  8211  oewordri  8212  nnmwordi  8255  omabs  8268  fisupg  8760  fiinfg  8957  cantnfle  9128  cantnflem1  9146  pr2ne  9425  gchina  10115  nqereu  10345  supsrlem  10527  1re  10635  lemul1a  11488  xlemul1a  12675  xrsupsslem  12694  xrinfmsslem  12695  xrub  12699  supxrunb1  12706  supxrunb2  12707  difelfzle  13014  addmodlteq  13308  seqcl2  13382  facdiv  13641  facwordi  13643  faclbnd  13644  pfxccat3  14090  dvdsabseq  15657  divgcdcoprm0  16003  2mulprm  16031  exprmfct  16042  prmfac1  16057  pockthg  16236  cply1mul  20456  mdetralt  21211  cmpsub  22002  fbfinnfr  22443  alexsubALTlem2  22650  alexsubALTlem3  22651  ovolicc2lem3  24114  fta1g  24755  fta1  24891  mulcxp  25262  cxpcn3lem  25322  gausslemma2dlem4  25939  colinearalg  26690  upgrwlkdvdelem  27511  umgr2wlk  27722  clwwlknwwlksn  27810  clwwlknonex2lem2  27881  dmdbr5ati  30193  cvmlift3lem4  32564  dfon2lem9  33031  fscgr  33536  colinbtwnle  33574  broutsideof2  33578  a1i14  33643  a1i24  33644  ordcmp  33790  bj-peircestab  33883  wl-aleq  34769  itg2addnc  34940  filbcmb  35009  mpobi123f  35434  mptbi12f  35438  ac6s6  35444  ltrnid  37265  cdleme25dN  37486  nn0rppwr  39175  ntrneiiso  40434  ee323  40835  vd13  40928  vd23  40929  ee03  41068  ee23an  41084  ee32  41086  ee32an  41088  ee123  41090  iccpartgt  43580  stgoldbwt  43934  tgoldbach  43975  nzerooringczr  44336