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  1735  equvel  2460  propeqop  5511  funopsn  7167  xpexr  7941  resf1extb  7957  omordi  8605  omwordi  8610  odi  8618  omass  8619  oen0  8625  oewordi  8630  oewordri  8631  nnmwordi  8674  omabs  8690  fisupg  9325  fiinfg  9540  cantnfle  9712  cantnflem1  9730  pr2neOLD  10046  gchina  10740  nqereu  10970  supsrlem  11152  1re  11262  lemul1a  12122  xlemul1a  13331  xrsupsslem  13350  xrinfmsslem  13351  xrub  13355  supxrunb1  13362  supxrunb2  13363  difelfzle  13682  addmodlteq  13988  seqcl2  14062  facdiv  14327  facwordi  14329  faclbnd  14330  pfxccat3  14773  dvdsabseq  16351  nn0rppwr  16599  divgcdcoprm0  16703  2mulprm  16731  exprmfct  16742  prmfac1  16758  pockthg  16945  nzerooringczr  21492  cply1mul  22301  mdetralt  22615  cmpsub  23409  fbfinnfr  23850  alexsubALTlem2  24057  alexsubALTlem3  24058  ovolicc2lem3  25555  dvfsumlem2  26068  fta1g  26210  fta1  26351  taylply2  26410  mulcxp  26728  cxpcn3lem  26791  gausslemma2dlem4  27414  colinearalg  28926  upgrwlkdvdelem  29757  umgr2wlk  29970  clwwlknwwlksn  30058  clwwlknonex2lem2  30128  dmdbr5ati  32442  cvmlift3lem4  35328  dfon2lem9  35793  fscgr  36082  colinbtwnle  36120  broutsideof2  36124  a1i14  36302  a1i24  36303  ordcmp  36449  bj-peircestab  36555  wl-aleq  37537  itg2addnc  37682  filbcmb  37748  mpobi123f  38170  mptbi12f  38174  ac6s6  38180  ltrnid  40138  cdleme25dN  40359  ntrneiiso  44109  ee323  44533  vd13  44626  vd23  44627  ee03  44766  ee23an  44782  ee32  44784  ee32an  44786  ee123  44788  iccpartgt  47419  stgoldbwt  47768  tgoldbach  47809