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  1733  equvel  2459  propeqop  5517  funopsn  7168  xpexr  7941  omordi  8603  omwordi  8608  odi  8616  omass  8617  oen0  8623  oewordi  8628  oewordri  8629  nnmwordi  8672  omabs  8688  fisupg  9322  fiinfg  9537  cantnfle  9709  cantnflem1  9727  pr2neOLD  10043  gchina  10737  nqereu  10967  supsrlem  11149  1re  11259  lemul1a  12119  xlemul1a  13327  xrsupsslem  13346  xrinfmsslem  13347  xrub  13351  supxrunb1  13358  supxrunb2  13359  difelfzle  13678  addmodlteq  13984  seqcl2  14058  facdiv  14323  facwordi  14325  faclbnd  14326  pfxccat3  14769  dvdsabseq  16347  nn0rppwr  16595  divgcdcoprm0  16699  2mulprm  16727  exprmfct  16738  prmfac1  16754  pockthg  16940  nzerooringczr  21509  cply1mul  22316  mdetralt  22630  cmpsub  23424  fbfinnfr  23865  alexsubALTlem2  24072  alexsubALTlem3  24073  ovolicc2lem3  25568  dvfsumlem2  26082  fta1g  26224  fta1  26365  taylply2  26424  mulcxp  26742  cxpcn3lem  26805  gausslemma2dlem4  27428  colinearalg  28940  upgrwlkdvdelem  29769  umgr2wlk  29979  clwwlknwwlksn  30067  clwwlknonex2lem2  30137  dmdbr5ati  32451  cvmlift3lem4  35307  dfon2lem9  35773  fscgr  36062  colinbtwnle  36100  broutsideof2  36104  a1i14  36283  a1i24  36284  ordcmp  36430  bj-peircestab  36536  wl-aleq  37516  itg2addnc  37661  filbcmb  37727  mpobi123f  38149  mptbi12f  38153  ac6s6  38159  ltrnid  40118  cdleme25dN  40339  ntrneiiso  44081  ee323  44506  vd13  44599  vd23  44600  ee03  44739  ee23an  44755  ee32  44757  ee32an  44759  ee123  44761  iccpartgt  47352  stgoldbwt  47701  tgoldbach  47742