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  5463  funopsn  7103  xpexr  7870  resf1extb  7886  omordi  8503  omwordi  8508  odi  8516  omass  8517  oen0  8524  oewordi  8529  oewordri  8530  nnmwordi  8573  omabs  8589  fisupg  9200  fiinfg  9416  cantnfle  9592  cantnflem1  9610  gchina  10622  nqereu  10852  supsrlem  11034  1re  11144  lemul1a  12007  xlemul1a  13215  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  supxrunb1  13246  supxrunb2  13247  difelfzle  13569  addmodlteq  13881  seqcl2  13955  facdiv  14222  facwordi  14224  faclbnd  14225  pfxccat3  14669  dvdsabseq  16252  nn0rppwr  16500  divgcdcoprm0  16604  2mulprm  16632  exprmfct  16643  prmfac1  16659  pockthg  16846  nzerooringczr  21447  cply1mul  22252  mdetralt  22564  cmpsub  23356  fbfinnfr  23797  alexsubALTlem2  24004  alexsubALTlem3  24005  ovolicc2lem3  25488  dvfsumlem2  26001  fta1g  26143  fta1  26284  taylply2  26343  mulcxp  26662  cxpcn3lem  26725  gausslemma2dlem4  27348  colinearalg  28995  upgrwlkdvdelem  29821  umgr2wlk  30034  clwwlknwwlksn  30125  clwwlknonex2lem2  30195  dmdbr5ati  32510  cvmlift3lem4  35538  antnestlaw2  35908  dfon2lem9  36005  fscgr  36296  colinbtwnle  36334  broutsideof2  36338  a1i14  36516  a1i24  36517  ordcmp  36663  bj-peircestab  36775  wl-aleq  37790  itg2addnc  37925  filbcmb  37991  mpobi123f  38413  mptbi12f  38417  ac6s6  38423  ltrnid  40511  cdleme25dN  40732  ntrneiiso  44447  ee323  44864  vd13  44957  vd23  44958  ee03  45096  ee23an  45112  ee32  45114  ee32an  45116  ee123  45118  iccpartgt  47787  stgoldbwt  48136  tgoldbach  48177  gpgedg2iv  48427