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  1768  equvel  2485  propeqop  5479  funopsnOLD  7157  xpexr  7934  resf1extb  7950  omordi  8582  omwordi  8587  odi  8595  omass  8596  oen0  8603  oewordi  8608  oewordri  8609  nnmwordi  8652  omabs  8668  fisupg  9287  fiinfg  9500  cantnfle  9679  cantnflem1  9697  gchina  10791  nqereu  11021  supsrlem  11203  1re  11315  lemul1a  12178  xlemul1a  13425  xrsupsslem  13444  xrinfmsslem  13445  xrub  13449  supxrunb1  13456  supxrunb2  13457  difelfzle  13782  addmodlteq  14096  seqcl2  14170  facdiv  14438  facwordi  14440  faclbnd  14441  pfxccat3  14891  dvdsabseq  16492  nn0rppwr  16744  divgcdcoprm0  16849  2mulprm  16877  exprmfct  16889  prmfac1  16905  pockthg  17093  nzerooringczr  21795  cply1mul  22623  mdetralt  22932  cmpsub  23727  fbfinnfr  24169  alexsubALTlem2  24376  alexsubALTlem3  24377  ovolicc2lem3  25849  dvfsumlem2  26356  fta1g  26497  fta1  26638  taylply2  26704  mulcxp  27022  cxpcn3lem  27084  gausslemma2dlem4  27705  colinearalg  29497  upgrwlkdvdelem  30331  umgr2wlk  30547  clwwlknwwlksn  30638  clwwlknonex2lem2  30708  dmdbr5ati  33033  cvmlift3lem4  36205  antnestlaw2  36575  dfon2lem9  36677  fscgr  36969  colinbtwnle  37007  broutsideof2  37011  a1i14  37213  a1i24  37214  ordcmp  37359  bj-peircestab  37544  wl-aleq  38604  itg2addnc  38729  filbcmb  38811  mpobi123f  39231  mptbi12f  39235  ac6s6  39241  ltrnid  41329  cdleme25dN  41550  ntrneiiso  45228  ee323  45627  vd13  45720  vd23  45721  ee03  45859  ee23an  45875  ee32  45877  ee32an  45879  ee123  45881  tmachlem-agreeprod  48083  iccpartgt  48645  stgoldbwt  49010  tgoldbach  49051  gpgedg2iv  49301