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 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

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  52  merco2  1763  equvel  2494  propeqop  5491  funopsnOLD  7146  xpexr  7914  resf1extb  7930  omordi  8550  omwordi  8555  odi  8563  omass  8564  oen0  8571  oewordi  8576  oewordri  8577  nnmwordi  8620  omabs  8636  fisupg  9247  fiinfg  9460  cantnfle  9639  cantnflem1  9657  gchina  10683  nqereu  10913  supsrlem  11095  1re  11207  lemul1a  12068  xlemul1a  13313  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  supxrunb1  13344  supxrunb2  13345  difelfzle  13668  addmodlteq  13981  seqcl2  14055  facdiv  14322  facwordi  14324  faclbnd  14325  pfxccat3  14770  dvdsabseq  16370  nn0rppwr  16618  divgcdcoprm0  16722  2mulprm  16750  exprmfct  16762  prmfac1  16778  pockthg  16965  nzerooringczr  21598  cply1mul  22424  mdetralt  22733  cmpsub  23525  fbfinnfr  23966  alexsubALTlem2  24173  alexsubALTlem3  24174  ovolicc2lem3  25646  dvfsumlem2  26154  fta1g  26295  fta1  26437  taylply2  26496  mulcxp  26815  cxpcn3lem  26877  gausslemma2dlem4  27498  colinearalg  29200  upgrwlkdvdelem  30025  umgr2wlk  30238  clwwlknwwlksn  30329  clwwlknonex2lem2  30399  dmdbr5ati  32714  cvmlift3lem4  35712  antnestlaw2  36082  dfon2lem9  36179  fscgr  36470  colinbtwnle  36508  broutsideof2  36512  a1i14  36700  a1i24  36701  ordcmp  36846  bj-peircestab  37031  wl-aleq  38077  itg2addnc  38212  filbcmb  38278  mpobi123f  38700  mptbi12f  38704  ac6s6  38710  ltrnid  40798  cdleme25dN  41019  ntrneiiso  44708  ee323  45108  vd13  45201  vd23  45202  ee03  45340  ee23an  45356  ee32  45358  ee32an  45360  ee123  45362  iccpartgt  48064  stgoldbwt  48429  tgoldbach  48470  gpgedg2iv  48720