Theorem simp2bi 1016

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2bi	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1013	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105   ∧ w3a 981

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 983

This theorem is referenced by:  0ellim  4449  smodm  6384  erdm  6637  ixpfn  6798  dif1en  6983  eluzelz  9664  elfz3nn0  10244  ef01bndlem  12111  sin01bnd  12112  cos01bnd  12113  sin01gt0  12117  bitsss  12300  gznegcl  12742  gzcjcl  12743  gzaddcl  12744  gzmulcl  12745  gzabssqcl  12748  4sqlem4a  12758  xpsff1o  13225  subgss  13554  rngmgp  13742  srgmgp  13774  ringmgp  13808  lmodring  14101  lmodprop2d  14154  reeff1oleme  15288  cosq14gt0  15348  cosq23lt0  15349  coseq0q4123  15350  coseq00topi  15351  coseq0negpitopi  15352  cosq34lt1  15366  cos02pilt1  15367  ioocosf1o  15370  gausslemma2dlem1a  15579  2sqlem2  15636  2sqlem3  15638