Theorem a1dd 50

Description: Double deduction introducing an antecedent. Deduction associated with a1d 25. 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 35	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  51  merco2  1736  equvel  2454  propeqop  5450  funopsn  7082  xpexr  7851  resf1extb  7867  omordi  8484  omwordi  8489  odi  8497  omass  8498  oen0  8504  oewordi  8509  oewordri  8510  nnmwordi  8553  omabs  8569  fisupg  9177  fiinfg  9391  cantnfle  9567  cantnflem1  9585  gchina  10593  nqereu  10823  supsrlem  11005  1re  11115  lemul1a  11978  xlemul1a  13190  xrsupsslem  13209  xrinfmsslem  13210  xrub  13214  supxrunb1  13221  supxrunb2  13222  difelfzle  13544  addmodlteq  13853  seqcl2  13927  facdiv  14194  facwordi  14196  faclbnd  14197  pfxccat3  14640  dvdsabseq  16224  nn0rppwr  16472  divgcdcoprm0  16576  2mulprm  16604  exprmfct  16615  prmfac1  16631  pockthg  16818  nzerooringczr  21387  cply1mul  22181  mdetralt  22493  cmpsub  23285  fbfinnfr  23726  alexsubALTlem2  23933  alexsubALTlem3  23934  ovolicc2lem3  25418  dvfsumlem2  25931  fta1g  26073  fta1  26214  taylply2  26273  mulcxp  26592  cxpcn3lem  26655  gausslemma2dlem4  27278  colinearalg  28855  upgrwlkdvdelem  29681  umgr2wlk  29894  clwwlknwwlksn  29982  clwwlknonex2lem2  30052  dmdbr5ati  32366  cvmlift3lem4  35299  antnestlaw2  35669  dfon2lem9  35769  fscgr  36058  colinbtwnle  36096  broutsideof2  36100  a1i14  36278  a1i24  36279  ordcmp  36425  bj-peircestab  36531  wl-aleq  37513  itg2addnc  37658  filbcmb  37724  mpobi123f  38146  mptbi12f  38150  ac6s6  38156  ltrnid  40118  cdleme25dN  40339  ntrneiiso  44068  ee323  44486  vd13  44579  vd23  44580  ee03  44718  ee23an  44734  ee32  44736  ee32an  44738  ee123  44740  iccpartgt  47415  stgoldbwt  47764  tgoldbach  47805  gpgedg2iv  48055