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  2460  propeqop  5461  funopsnOLD  7102  xpexr  7869  resf1extb  7885  omordi  8501  omwordi  8506  odi  8514  omass  8515  oen0  8522  oewordi  8527  oewordri  8528  nnmwordi  8571  omabs  8587  fisupg  9198  fiinfg  9414  cantnfle  9592  cantnflem1  9610  gchina  10622  nqereu  10852  supsrlem  11034  1re  11144  lemul1a  12009  xlemul1a  13240  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  supxrunb1  13271  supxrunb2  13272  difelfzle  13595  addmodlteq  13908  seqcl2  13982  facdiv  14249  facwordi  14251  faclbnd  14252  pfxccat3  14696  dvdsabseq  16282  nn0rppwr  16530  divgcdcoprm0  16634  2mulprm  16662  exprmfct  16674  prmfac1  16690  pockthg  16877  nzerooringczr  21460  cply1mul  22261  mdetralt  22573  cmpsub  23365  fbfinnfr  23806  alexsubALTlem2  24013  alexsubALTlem3  24014  ovolicc2lem3  25486  dvfsumlem2  25994  fta1g  26135  fta1  26274  taylply2  26333  mulcxp  26649  cxpcn3lem  26711  gausslemma2dlem4  27332  colinearalg  28979  upgrwlkdvdelem  29804  umgr2wlk  30017  clwwlknwwlksn  30108  clwwlknonex2lem2  30178  dmdbr5ati  32493  cvmlift3lem4  35504  antnestlaw2  35874  dfon2lem9  35971  fscgr  36262  colinbtwnle  36300  broutsideof2  36304  a1i14  36482  a1i24  36483  ordcmp  36629  bj-peircestab  36815  wl-aleq  37860  itg2addnc  37995  filbcmb  38061  mpobi123f  38483  mptbi12f  38487  ac6s6  38493  ltrnid  40581  cdleme25dN  40802  ntrneiiso  44518  ee323  44935  vd13  45028  vd23  45029  ee03  45167  ee23an  45183  ee32  45185  ee32an  45187  ee123  45189  iccpartgt  47887  stgoldbwt  48252  tgoldbach  48293  gpgedg2iv  48543