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  1738  equvel  2468  propeqop  5362  funopsn  6887  xpexr  7605  omordi  8175  omwordi  8180  odi  8188  omass  8189  oen0  8195  oewordi  8200  oewordri  8201  nnmwordi  8244  omabs  8257  fisupg  8750  fiinfg  8947  cantnfle  9118  cantnflem1  9136  pr2ne  9416  gchina  10110  nqereu  10340  supsrlem  10522  1re  10630  lemul1a  11483  xlemul1a  12669  xrsupsslem  12688  xrinfmsslem  12689  xrub  12693  supxrunb1  12700  supxrunb2  12701  difelfzle  13015  addmodlteq  13309  seqcl2  13384  facdiv  13643  facwordi  13645  faclbnd  13646  pfxccat3  14087  dvdsabseq  15655  divgcdcoprm0  15999  2mulprm  16027  exprmfct  16038  prmfac1  16053  pockthg  16232  cply1mul  20923  mdetralt  21213  cmpsub  22005  fbfinnfr  22446  alexsubALTlem2  22653  alexsubALTlem3  22654  ovolicc2lem3  24123  fta1g  24768  fta1  24904  mulcxp  25276  cxpcn3lem  25336  gausslemma2dlem4  25953  colinearalg  26704  upgrwlkdvdelem  27525  umgr2wlk  27735  clwwlknwwlksn  27823  clwwlknonex2lem2  27893  dmdbr5ati  30205  cvmlift3lem4  32682  dfon2lem9  33149  fscgr  33654  colinbtwnle  33692  broutsideof2  33696  a1i14  33761  a1i24  33762  ordcmp  33908  bj-peircestab  34001  wl-aleq  34940  itg2addnc  35111  filbcmb  35178  mpobi123f  35600  mptbi12f  35604  ac6s6  35610  ltrnid  37431  cdleme25dN  37652  nn0rppwr  39490  ntrneiiso  40794  ee323  41214  vd13  41307  vd23  41308  ee03  41447  ee23an  41463  ee32  41465  ee32an  41467  ee123  41469  iccpartgt  43944  stgoldbwt  44294  tgoldbach  44335  nzerooringczr  44696