Theorem simp2d 1037

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 1025	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜒)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simp2bi  1040  erinxp  6845  resixp  6970  exmidapne  7579  addcanprleml  7934  addcanprlemu  7935  ltmprr  7962  lelttrdi  8705  ixxdisj  10242  ixxss1  10243  ixxss2  10244  ixxss12  10245  iccgelb  10271  iccss2  10283  icodisj  10331  ioom  10627  elicore  10633  flqdiv  10690  mulqaddmodid  10733  modsumfzodifsn  10765  addmodlteq  10767  immul  11572  sumtp  12108  crth  12929  phimullem  12930  eulerthlem1  12932  eulerthlema  12935  eulerthlemh  12936  eulerthlemth  12937  ballotfilemcdc  13150  ballotfilemfc0  13157  ctiunct  13212  structn0fun  13246  strleund  13337  strext  13339  mhmlin  13701  subm0cl  13712  eqger  13962  eqgcpbl  13966  lmodvsdi  14508  lss0cl  14566  rnglidlmsgrp  14694  2idlcpblrng  14720  lmcl  15159  lmtopcnp  15164  xmeter  15350  tgqioo  15469  ivthinclemlopn  15550  ivthinclemuopn  15552  limcimolemlt  15578  limcresi  15580  limccnpcntop  15589  limccnp2lem  15590  limccnp2cntop  15591  cosordlem  15763  perfectlem2  15917  subgruhgredgdm  16314  subumgredg2en  16315  wlkp  16378  wlkpg  16379  wlkvtxiedg  16389  wlk1walkdom  16403  upgr2wlkdc  16421  isclwwlkn  16457  clwwlknwrd  16458  clwwlknon  16473  clwwlknonex2e  16484  trlsegvdeglem3  16506  trlsegvdeglem5  16508  eupth2lem3fi  16520  depindlem2  16551  depindlem3  16552  depind  16553