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  2461  propeqop  5456  funopsn  7096  xpexr  7863  resf1extb  7879  omordi  8495  omwordi  8500  odi  8508  omass  8509  oen0  8516  oewordi  8521  oewordri  8522  nnmwordi  8565  omabs  8581  fisupg  9192  fiinfg  9408  cantnfle  9586  cantnflem1  9604  gchina  10616  nqereu  10846  supsrlem  11028  1re  11138  lemul1a  12003  xlemul1a  13234  xrsupsslem  13253  xrinfmsslem  13254  xrub  13258  supxrunb1  13265  supxrunb2  13266  difelfzle  13589  addmodlteq  13902  seqcl2  13976  facdiv  14243  facwordi  14245  faclbnd  14246  pfxccat3  14690  dvdsabseq  16276  nn0rppwr  16524  divgcdcoprm0  16628  2mulprm  16656  exprmfct  16668  prmfac1  16684  pockthg  16871  nzerooringczr  21473  cply1mul  22274  mdetralt  22586  cmpsub  23378  fbfinnfr  23819  alexsubALTlem2  24026  alexsubALTlem3  24027  ovolicc2lem3  25499  dvfsumlem2  26007  fta1g  26148  fta1  26288  taylply2  26347  mulcxp  26665  cxpcn3lem  26727  gausslemma2dlem4  27349  colinearalg  28996  upgrwlkdvdelem  29822  umgr2wlk  30035  clwwlknwwlksn  30126  clwwlknonex2lem2  30196  dmdbr5ati  32511  cvmlift3lem4  35523  antnestlaw2  35893  dfon2lem9  35990  fscgr  36281  colinbtwnle  36319  broutsideof2  36323  a1i14  36501  a1i24  36502  ordcmp  36648  bj-peircestab  36834  wl-aleq  37877  itg2addnc  38012  filbcmb  38078  mpobi123f  38500  mptbi12f  38504  ac6s6  38510  ltrnid  40598  cdleme25dN  40819  ntrneiiso  44539  ee323  44956  vd13  45049  vd23  45050  ee03  45188  ee23an  45204  ee32  45206  ee32an  45208  ee123  45210  iccpartgt  47902  stgoldbwt  48267  tgoldbach  48308  gpgedg2iv  48558