Theorem simp2d 1036

Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)

Hypothesis

Ref	Expression
3simp1d.1	⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2d	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp2 1024	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  simp2bi  1039  erinxp  6778  resixp  6902  exmidapne  7479  addcanprleml  7834  addcanprlemu  7835  ltmprr  7862  lelttrdi  8606  ixxdisj  10138  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccgelb  10167  iccss2  10179  icodisj  10227  ioom  10521  elicore  10527  flqdiv  10584  mulqaddmodid  10627  modsumfzodifsn  10659  addmodlteq  10661  immul  11441  sumtp  11977  crth  12798  phimullem  12799  eulerthlem1  12801  eulerthlema  12804  eulerthlemh  12805  eulerthlemth  12806  ctiunct  13063  structn0fun  13097  strleund  13188  strext  13190  mhmlin  13552  subm0cl  13563  eqger  13813  eqgcpbl  13817  lmodvsdi  14328  lss0cl  14386  rnglidlmsgrp  14514  2idlcpblrng  14540  lmcl  14972  lmtopcnp  14977  xmeter  15163  tgqioo  15282  ivthinclemlopn  15363  ivthinclemuopn  15365  limcimolemlt  15391  limcresi  15393  limccnpcntop  15402  limccnp2lem  15403  limccnp2cntop  15404  cosordlem  15576  perfectlem2  15727  subgruhgredgdm  16124  subumgredg2en  16125  wlkp  16188  wlkpg  16189  wlkvtxiedg  16199  wlk1walkdom  16213  upgr2wlkdc  16231  isclwwlkn  16267  clwwlknwrd  16268  clwwlknon  16283  clwwlknonex2e  16294  trlsegvdeglem3  16316  trlsegvdeglem5  16318  eupth2lem3fi  16330  depindlem2  16347  depindlem3  16348  depind  16349