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  2485  propeqop  5484  funopsnOLD  7146  xpexr  7916  resf1extb  7932  omordi  8554  omwordi  8559  odi  8567  omass  8568  oen0  8575  oewordi  8580  oewordri  8581  nnmwordi  8624  omabs  8640  fisupg  9259  fiinfg  9472  cantnfle  9651  cantnflem1  9669  gchina  10709  nqereu  10939  supsrlem  11121  1re  11233  lemul1a  12094  xlemul1a  13341  xrsupsslem  13360  xrinfmsslem  13361  xrub  13365  supxrunb1  13372  supxrunb2  13373  difelfzle  13697  addmodlteq  14011  seqcl2  14085  facdiv  14352  facwordi  14354  faclbnd  14355  pfxccat3  14804  dvdsabseq  16404  nn0rppwr  16652  divgcdcoprm0  16756  2mulprm  16784  exprmfct  16796  prmfac1  16812  pockthg  16999  nzerooringczr  21694  cply1mul  22522  mdetralt  22831  cmpsub  23626  fbfinnfr  24068  alexsubALTlem2  24275  alexsubALTlem3  24276  ovolicc2lem3  25748  dvfsumlem2  26255  fta1g  26396  fta1  26539  taylply2  26605  mulcxp  26923  cxpcn3lem  26985  gausslemma2dlem4  27606  colinearalg  29368  upgrwlkdvdelem  30202  umgr2wlk  30418  clwwlknwwlksn  30509  clwwlknonex2lem2  30579  dmdbr5ati  32904  cvmlift3lem4  35902  antnestlaw2  36272  dfon2lem9  36369  fscgr  36661  colinbtwnle  36699  broutsideof2  36703  a1i14  36921  a1i24  36922  ordcmp  37067  bj-peircestab  37252  wl-aleq  38299  itg2addnc  38424  filbcmb  38491  mpobi123f  38911  mptbi12f  38915  ac6s6  38921  ltrnid  41009  cdleme25dN  41230  ntrneiiso  44932  ee323  45332  vd13  45425  vd23  45426  ee03  45564  ee23an  45580  ee32  45582  ee32an  45584  ee123  45586  tmachlem-agreeprod  47766  iccpartgt  48328  stgoldbwt  48693  tgoldbach  48734  gpgedg2iv  48984