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  1737  equvel  2456  propeqop  5445  funopsn  7081  xpexr  7848  resf1extb  7864  omordi  8481  omwordi  8486  odi  8494  omass  8495  oen0  8501  oewordi  8506  oewordri  8507  nnmwordi  8550  omabs  8566  fisupg  9172  fiinfg  9385  cantnfle  9561  cantnflem1  9579  gchina  10590  nqereu  10820  supsrlem  11002  1re  11112  lemul1a  11975  xlemul1a  13187  xrsupsslem  13206  xrinfmsslem  13207  xrub  13211  supxrunb1  13218  supxrunb2  13219  difelfzle  13541  addmodlteq  13853  seqcl2  13927  facdiv  14194  facwordi  14196  faclbnd  14197  pfxccat3  14641  dvdsabseq  16224  nn0rppwr  16472  divgcdcoprm0  16576  2mulprm  16604  exprmfct  16615  prmfac1  16631  pockthg  16818  nzerooringczr  21417  cply1mul  22211  mdetralt  22523  cmpsub  23315  fbfinnfr  23756  alexsubALTlem2  23963  alexsubALTlem3  23964  ovolicc2lem3  25447  dvfsumlem2  25960  fta1g  26102  fta1  26243  taylply2  26302  mulcxp  26621  cxpcn3lem  26684  gausslemma2dlem4  27307  colinearalg  28888  upgrwlkdvdelem  29714  umgr2wlk  29927  clwwlknwwlksn  30018  clwwlknonex2lem2  30088  dmdbr5ati  32402  cvmlift3lem4  35366  antnestlaw2  35736  dfon2lem9  35833  fscgr  36124  colinbtwnle  36162  broutsideof2  36166  a1i14  36344  a1i24  36345  ordcmp  36491  bj-peircestab  36597  wl-aleq  37579  itg2addnc  37724  filbcmb  37790  mpobi123f  38212  mptbi12f  38216  ac6s6  38222  ltrnid  40244  cdleme25dN  40465  ntrneiiso  44194  ee323  44611  vd13  44704  vd23  44705  ee03  44843  ee23an  44859  ee32  44861  ee32an  44863  ee123  44865  iccpartgt  47537  stgoldbwt  47886  tgoldbach  47927  gpgedg2iv  48177