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  1756  equvel  2487  propeqop  5476  funopsnOLD  7131  xpexr  7899  resf1extb  7915  omordi  8535  omwordi  8540  odi  8548  omass  8549  oen0  8556  oewordi  8561  oewordri  8562  nnmwordi  8605  omabs  8621  fisupg  9232  fiinfg  9447  cantnfle  9626  cantnflem1  9644  gchina  10657  nqereu  10887  supsrlem  11069  1re  11181  lemul1a  12045  xlemul1a  13291  xrsupsslem  13310  xrinfmsslem  13311  xrub  13315  supxrunb1  13322  supxrunb2  13323  difelfzle  13646  addmodlteq  13959  seqcl2  14033  facdiv  14300  facwordi  14302  faclbnd  14303  pfxccat3  14747  dvdsabseq  16347  nn0rppwr  16595  divgcdcoprm0  16699  2mulprm  16727  exprmfct  16739  prmfac1  16755  pockthg  16942  nzerooringczr  21532  cply1mul  22359  mdetralt  22668  cmpsub  23460  fbfinnfr  23901  alexsubALTlem2  24108  alexsubALTlem3  24109  ovolicc2lem3  25581  dvfsumlem2  26089  fta1g  26230  fta1  26372  taylply2  26431  mulcxp  26750  cxpcn3lem  26812  gausslemma2dlem4  27433  colinearalg  29111  upgrwlkdvdelem  29936  umgr2wlk  30149  clwwlknwwlksn  30240  clwwlknonex2lem2  30310  dmdbr5ati  32625  cvmlift3lem4  35672  antnestlaw2  36042  dfon2lem9  36139  fscgr  36430  colinbtwnle  36468  broutsideof2  36472  a1i14  36660  a1i24  36661  ordcmp  36807  bj-peircestab  36993  wl-aleq  38038  itg2addnc  38173  filbcmb  38239  mpobi123f  38661  mptbi12f  38665  ac6s6  38671  ltrnid  40759  cdleme25dN  40980  ntrneiiso  44667  ee323  45084  vd13  45177  vd23  45178  ee03  45316  ee23an  45332  ee32  45334  ee32an  45336  ee123  45338  iccpartgt  48033  stgoldbwt  48398  tgoldbach  48439  gpgedg2iv  48689