Theorem simp2bi 1013

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 1010	1 ⊢ (𝜑 → 𝜒)

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

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 980

This theorem is referenced by:  0ellim  4400  smodm  6294  erdm  6547  ixpfn  6706  dif1en  6881  eluzelz  9539  elfz3nn0  10117  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  gznegcl  12375  gzcjcl  12376  gzaddcl  12377  gzmulcl  12378  gzabssqcl  12381  4sqlem4a  12391  xpsff1o  12773  subgss  13039  srgmgp  13156  ringmgp  13190  lmodring  13390  lmodprop2d  13443  reeff1oleme  14232  cosq14gt0  14292  cosq23lt0  14293  coseq0q4123  14294  coseq00topi  14295  coseq0negpitopi  14296  cosq34lt1  14310  cos02pilt1  14311  ioocosf1o  14314  2sqlem2  14501  2sqlem3  14503