Theorem a1dd 51

Description: Double deduction introducing an antecedent. Deduction associated with a1d 26. 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 36	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2a1dd  52  merco2  1769  equvel  2486  propeqop  5479  funopsnOLD  7152  xpexr  7930  resf1extb  7946  omordi  8574  omwordi  8579  odi  8587  omass  8588  oen0  8595  oewordi  8600  oewordri  8601  nnmwordi  8644  omabs  8660  fisupg  9279  fiinfg  9493  cantnfle  9672  cantnflem1  9690  gchina  10784  nqereu  11014  supsrlem  11196  1re  11308  lemul1a  12171  xlemul1a  13418  xrsupsslem  13437  xrinfmsslem  13438  xrub  13442  supxrunb1  13449  supxrunb2  13450  difelfzle  13775  addmodlteq  14089  seqcl2  14163  facdiv  14431  facwordi  14433  faclbnd  14434  pfxccat3  14883  dvdsabseq  16483  nn0rppwr  16735  divgcdcoprm0  16840  2mulprm  16868  exprmfct  16880  prmfac1  16896  pockthg  17084  nzerooringczr  21786  cply1mul  22614  mdetralt  22923  cmpsub  23718  fbfinnfr  24160  alexsubALTlem2  24367  alexsubALTlem3  24368  ovolicc2lem3  25840  dvfsumlem2  26347  fta1g  26488  fta1  26629  taylply2  26695  mulcxp  27013  cxpcn3lem  27075  gausslemma2dlem4  27696  colinearalg  29488  upgrwlkdvdelem  30322  umgr2wlk  30538  clwwlknwwlksn  30629  clwwlknonex2lem2  30699  dmdbr5ati  33024  cvmlift3lem4  36087  antnestlaw2  36457  dfon2lem9  36553  fscgr  36845  colinbtwnle  36883  broutsideof2  36887  a1i14  37089  a1i24  37090  ordcmp  37235  bj-peircestab  37420  wl-aleq  38467  itg2addnc  38592  filbcmb  38674  mpobi123f  39094  mptbi12f  39098  ac6s6  39104  ltrnid  41192  cdleme25dN  41413  ntrneiiso  45090  ee323  45490  vd13  45583  vd23  45584  ee03  45722  ee23an  45738  ee32  45740  ee32an  45742  ee123  45744  tmachlem-agreeprod  47946  iccpartgt  48508  stgoldbwt  48873  tgoldbach  48914  gpgedg2iv  49164