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  6856  resixp  6981  exmidapne  7590  addcanprleml  7945  addcanprlemu  7946  ltmprr  7973  lelttrdi  8718  ixxdisj  10258  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccgelb  10287  iccss2  10299  icodisj  10347  ioom  10647  elicore  10653  flqdiv  10710  mulqaddmodid  10753  modsumfzodifsn  10785  addmodlteq  10787  immul  11592  sumtp  12128  crth  12949  phimullem  12950  eulerthlem1  12952  eulerthlema  12955  eulerthlemh  12956  eulerthlemth  12957  ballotfilemcdc  13170  ballotfilemfc0  13179  ballotfilemro  13213  ctiunct  13278  structn0fun  13312  strleund  13403  strext  13405  mhmlin  13725  subm0cl  13736  eqger  13980  eqgcpbl  13984  lmodvsdi  14588  lss0cl  14646  rnglidlmsgrp  14774  2idlcpblrng  14800  lmcl  15239  lmtopcnp  15244  xmeter  15430  tgqioo  15549  ivthinclemlopn  15630  ivthinclemuopn  15632  limcimolemlt  15658  limcresi  15660  limccnpcntop  15669  limccnp2lem  15670  limccnp2cntop  15671  cosordlem  15843  perfectlem2  15997  subgruhgredgdm  16394  subumgredg2en  16395  wlkp  16458  wlkpg  16459  wlkvtxiedg  16469  wlk1walkdom  16483  upgr2wlkdc  16501  isclwwlkn  16537  clwwlknwrd  16538  clwwlknon  16553  clwwlknonex2e  16564  trlsegvdeglem3  16586  trlsegvdeglem5  16588  eupth2lem3fi  16600  depindlem2  16631  depindlem3  16632  depind  16633