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  1737  equvel  2479  propeqop  5399  funopsn  6912  xpexr  7625  omordi  8194  omwordi  8199  odi  8207  omass  8208  oen0  8214  oewordi  8219  oewordri  8220  nnmwordi  8263  omabs  8276  fisupg  8768  fiinfg  8965  cantnfle  9136  cantnflem1  9154  pr2ne  9433  gchina  10123  nqereu  10353  supsrlem  10535  1re  10643  lemul1a  11496  xlemul1a  12684  xrsupsslem  12703  xrinfmsslem  12704  xrub  12708  supxrunb1  12715  supxrunb2  12716  difelfzle  13023  addmodlteq  13317  seqcl2  13391  facdiv  13650  facwordi  13652  faclbnd  13653  pfxccat3  14098  dvdsabseq  15665  divgcdcoprm0  16011  2mulprm  16039  exprmfct  16050  prmfac1  16065  pockthg  16244  cply1mul  20464  mdetralt  21219  cmpsub  22010  fbfinnfr  22451  alexsubALTlem2  22658  alexsubALTlem3  22659  ovolicc2lem3  24122  fta1g  24763  fta1  24899  mulcxp  25270  cxpcn3lem  25330  gausslemma2dlem4  25947  colinearalg  26698  upgrwlkdvdelem  27519  umgr2wlk  27730  clwwlknwwlksn  27818  clwwlknonex2lem2  27889  dmdbr5ati  30201  cvmlift3lem4  32571  dfon2lem9  33038  fscgr  33543  colinbtwnle  33581  broutsideof2  33585  a1i14  33650  a1i24  33651  ordcmp  33797  bj-peircestab  33890  wl-aleq  34777  itg2addnc  34948  filbcmb  35017  mpobi123f  35442  mptbi12f  35446  ac6s6  35452  ltrnid  37273  cdleme25dN  37494  nn0rppwr  39189  ntrneiiso  40448  ee323  40849  vd13  40942  vd23  40943  ee03  41082  ee23an  41098  ee32  41100  ee32an  41102  ee123  41104  iccpartgt  43594  stgoldbwt  43948  tgoldbach  43989  nzerooringczr  44350