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  1743  equvel  2464  propeqop  5448  funopsnOLD  7091  xpexr  7858  resf1extb  7874  omordi  8491  omwordi  8496  odi  8504  omass  8505  oen0  8512  oewordi  8517  oewordri  8518  nnmwordi  8561  omabs  8577  fisupg  9188  fiinfg  9404  cantnfle  9583  cantnflem1  9601  gchina  10613  nqereu  10843  supsrlem  11025  1re  11135  lemul1a  12000  xlemul1a  13231  xrsupsslem  13250  xrinfmsslem  13251  xrub  13255  supxrunb1  13262  supxrunb2  13263  difelfzle  13586  addmodlteq  13899  seqcl2  13973  facdiv  14240  facwordi  14242  faclbnd  14243  pfxccat3  14687  dvdsabseq  16273  nn0rppwr  16521  divgcdcoprm0  16625  2mulprm  16653  exprmfct  16665  prmfac1  16681  pockthg  16868  nzerooringczr  21455  cply1mul  22282  mdetralt  22591  cmpsub  23383  fbfinnfr  23824  alexsubALTlem2  24031  alexsubALTlem3  24032  ovolicc2lem3  25504  dvfsumlem2  26012  fta1g  26153  fta1  26292  taylply2  26351  mulcxp  26667  cxpcn3lem  26729  gausslemma2dlem4  27350  colinearalg  28997  upgrwlkdvdelem  29822  umgr2wlk  30035  clwwlknwwlksn  30126  clwwlknonex2lem2  30196  dmdbr5ati  32511  cvmlift3lem4  35550  antnestlaw2  35920  dfon2lem9  36017  fscgr  36308  colinbtwnle  36346  broutsideof2  36350  a1i14  36528  a1i24  36529  ordcmp  36675  bj-peircestab  36861  wl-aleq  37906  itg2addnc  38041  filbcmb  38107  mpobi123f  38529  mptbi12f  38533  ac6s6  38539  ltrnid  40627  cdleme25dN  40848  ntrneiiso  44535  ee323  44952  vd13  45045  vd23  45046  ee03  45184  ee23an  45200  ee32  45202  ee32an  45204  ee123  45206  iccpartgt  47902  stgoldbwt  48267  tgoldbach  48308  gpgedg2iv  48558