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  1739  equvel  2456  propeqop  5508  funopsn  7146  xpexr  7909  omordi  8566  omwordi  8571  odi  8579  omass  8580  oen0  8586  oewordi  8591  oewordri  8592  nnmwordi  8635  omabs  8650  fisupg  9291  fiinfg  9494  cantnfle  9666  cantnflem1  9684  pr2neOLD  10000  gchina  10694  nqereu  10924  supsrlem  11106  1re  11214  lemul1a  12068  xlemul1a  13267  xrsupsslem  13286  xrinfmsslem  13287  xrub  13291  supxrunb1  13298  supxrunb2  13299  difelfzle  13614  addmodlteq  13911  seqcl2  13986  facdiv  14247  facwordi  14249  faclbnd  14250  pfxccat3  14684  dvdsabseq  16256  divgcdcoprm0  16602  2mulprm  16630  exprmfct  16641  prmfac1  16658  pockthg  16839  cply1mul  21818  mdetralt  22110  cmpsub  22904  fbfinnfr  23345  alexsubALTlem2  23552  alexsubALTlem3  23553  ovolicc2lem3  25036  fta1g  25685  fta1  25821  mulcxp  26193  cxpcn3lem  26255  gausslemma2dlem4  26872  colinearalg  28168  upgrwlkdvdelem  28993  umgr2wlk  29203  clwwlknwwlksn  29291  clwwlknonex2lem2  29361  dmdbr5ati  31675  cvmlift3lem4  34313  dfon2lem9  34763  fscgr  35052  colinbtwnle  35090  broutsideof2  35094  gg-dvfsumlem2  35183  a1i14  35185  a1i24  35186  ordcmp  35332  bj-peircestab  35429  wl-aleq  36404  itg2addnc  36542  filbcmb  36608  mpobi123f  37030  mptbi12f  37034  ac6s6  37040  ltrnid  39006  cdleme25dN  39227  nn0rppwr  41224  ntrneiiso  42842  ee323  43269  vd13  43362  vd23  43363  ee03  43502  ee23an  43518  ee32  43520  ee32an  43522  ee123  43524  iccpartgt  46095  stgoldbwt  46444  tgoldbach  46485  nzerooringczr  46970