Theorem simp2bi 1014

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

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

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 981

This theorem is referenced by:  0ellim  4412  smodm  6309  erdm  6562  ixpfn  6721  dif1en  6896  eluzelz  9554  elfz3nn0  10132  ef01bndlem  11781  sin01bnd  11782  cos01bnd  11783  sin01gt0  11786  gznegcl  12390  gzcjcl  12391  gzaddcl  12392  gzmulcl  12393  gzabssqcl  12396  4sqlem4a  12406  xpsff1o  12790  subgss  13078  rngmgp  13250  srgmgp  13282  ringmgp  13316  lmodring  13571  lmodprop2d  13624  reeff1oleme  14576  cosq14gt0  14636  cosq23lt0  14637  coseq0q4123  14638  coseq00topi  14639  coseq0negpitopi  14640  cosq34lt1  14654  cos02pilt1  14655  ioocosf1o  14658  2sqlem2  14845  2sqlem3  14847