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  1766  equvel  2488  propeqop  5490  funopsnOLD  7145  xpexr  7911  resf1extb  7927  omordi  8547  omwordi  8552  odi  8560  omass  8561  oen0  8568  oewordi  8573  oewordri  8574  nnmwordi  8617  omabs  8633  fisupg  9244  fiinfg  9457  cantnfle  9636  cantnflem1  9654  gchina  10688  nqereu  10918  supsrlem  11100  1re  11212  lemul1a  12073  xlemul1a  13318  xrsupsslem  13337  xrinfmsslem  13338  xrub  13342  supxrunb1  13349  supxrunb2  13350  difelfzle  13674  addmodlteq  13987  seqcl2  14061  facdiv  14328  facwordi  14330  faclbnd  14331  pfxccat3  14776  dvdsabseq  16375  nn0rppwr  16623  divgcdcoprm0  16727  2mulprm  16755  exprmfct  16767  prmfac1  16783  pockthg  16970  nzerooringczr  21639  cply1mul  22465  mdetralt  22774  cmpsub  23566  fbfinnfr  24007  alexsubALTlem2  24214  alexsubALTlem3  24215  ovolicc2lem3  25687  dvfsumlem2  26195  fta1g  26336  fta1  26478  taylply2  26540  mulcxp  26859  cxpcn3lem  26921  gausslemma2dlem4  27542  colinearalg  29269  upgrwlkdvdelem  30094  umgr2wlk  30307  clwwlknwwlksn  30398  clwwlknonex2lem2  30468  dmdbr5ati  32783  cvmlift3lem4  35822  antnestlaw2  36192  dfon2lem9  36289  fscgr  36580  colinbtwnle  36618  broutsideof2  36622  a1i14  36840  a1i24  36841  ordcmp  36986  bj-peircestab  37171  wl-aleq  38218  itg2addnc  38353  filbcmb  38419  mpobi123f  38839  mptbi12f  38843  ac6s6  38849  ltrnid  40937  cdleme25dN  41158  ntrneiiso  44845  ee323  45245  vd13  45338  vd23  45339  ee03  45477  ee23an  45493  ee32  45495  ee32an  45497  ee123  45499  iccpartgt  48204  stgoldbwt  48569  tgoldbach  48610  gpgedg2iv  48860