Theorem simp2d 1041

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  simp2bi  1044  erinxp  6877  resixp  7009  exmidapne  7620  addcanprleml  7975  addcanprlemu  7976  ltmprr  8003  lelttrdi  8748  ixxdisj  10288  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccgelb  10317  iccss2  10329  icodisj  10377  ioom  10678  elicore  10684  flqdiv  10741  mulqaddmodid  10784  modsumfzodifsn  10816  addmodlteq  10818  immul  11627  sumtp  12164  crth  12985  phimullem  12986  eulerthlem1  12988  eulerthlema  12991  eulerthlemh  12992  eulerthlemth  12993  ballotfilemcdc  13206  ballotfilemfc0  13215  ballotfilemro  13249  ctiunct  13314  structn0fun  13348  strleund  13440  strext  13442  mhmlin  13757  subm0cl  13768  eqger  14010  eqgcpbl  14014  lmodvsdi  14631  lss0cl  14689  rnglidlmsgrp  14817  2idlcpblrng  14843  lmcl  15329  lmtopcnp  15334  xmeter  15520  tgqioo  15639  ivthinclemlopn  15720  ivthinclemuopn  15722  limcimolemlt  15748  limcresi  15750  limccnpcntop  15759  limccnp2lem  15760  limccnp2cntop  15761  cosordlem  15933  birthdaylem3  16072  perfectlem2  16097  subgruhgredgdm  16494  subumgredg2en  16495  wlkp  16558  wlkpg  16559  wlkvtxiedg  16569  wlk1walkdom  16583  upgr2wlkdc  16601  isclwwlkn  16637  clwwlknwrd  16638  clwwlknon  16653  clwwlknonex2e  16664  trlsegvdeglem3  16686  trlsegvdeglem5  16688  eupth2lem3fi  16700  depindlem2  16731  depindlem3  16732  depind  16733