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  2458  propeqop  5453  funopsn  7091  xpexr  7858  resf1extb  7874  omordi  8491  omwordi  8496  odi  8504  omass  8505  oen0  8512  oewordi  8517  oewordri  8518  nnmwordi  8561  omabs  8577  fisupg  9186  fiinfg  9402  cantnfle  9578  cantnflem1  9596  gchina  10608  nqereu  10838  supsrlem  11020  1re  11130  lemul1a  11993  xlemul1a  13201  xrsupsslem  13220  xrinfmsslem  13221  xrub  13225  supxrunb1  13232  supxrunb2  13233  difelfzle  13555  addmodlteq  13867  seqcl2  13941  facdiv  14208  facwordi  14210  faclbnd  14211  pfxccat3  14655  dvdsabseq  16238  nn0rppwr  16486  divgcdcoprm0  16590  2mulprm  16618  exprmfct  16629  prmfac1  16645  pockthg  16832  nzerooringczr  21433  cply1mul  22238  mdetralt  22550  cmpsub  23342  fbfinnfr  23783  alexsubALTlem2  23990  alexsubALTlem3  23991  ovolicc2lem3  25474  dvfsumlem2  25987  fta1g  26129  fta1  26270  taylply2  26329  mulcxp  26648  cxpcn3lem  26711  gausslemma2dlem4  27334  colinearalg  28932  upgrwlkdvdelem  29758  umgr2wlk  29971  clwwlknwwlksn  30062  clwwlknonex2lem2  30132  dmdbr5ati  32446  cvmlift3lem4  35465  antnestlaw2  35835  dfon2lem9  35932  fscgr  36223  colinbtwnle  36261  broutsideof2  36265  a1i14  36443  a1i24  36444  ordcmp  36590  bj-peircestab  36696  wl-aleq  37679  itg2addnc  37814  filbcmb  37880  mpobi123f  38302  mptbi12f  38306  ac6s6  38312  ltrnid  40334  cdleme25dN  40555  ntrneiiso  44274  ee323  44691  vd13  44784  vd23  44785  ee03  44923  ee23an  44939  ee32  44941  ee32an  44943  ee123  44945  iccpartgt  47615  stgoldbwt  47964  tgoldbach  48005  gpgedg2iv  48255