Theorem simp2bi 1040

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

Syntax hints:   → wi 4   ↔ wb 105   ∧ 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:  0ellim  4521  smodm  6524  erdm  6779  ixpfn  6941  dif1en  7138  eluzelz  9869  lincmble  10343  elfz3nn0  10456  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  sin01gt0  12456  bitsss  12639  gznegcl  13081  gzcjcl  13082  gzaddcl  13083  gzmulcl  13084  gzabssqcl  13087  4sqlem4a  13097  xpsff1o  13583  subgss  13912  rngmgp  14101  srgmgp  14133  ringmgp  14167  lmodring  14492  lmodprop2d  14545  reeff1oleme  15686  cosq14gt0  15746  cosq23lt0  15747  coseq0q4123  15748  coseq00topi  15749  coseq0negpitopi  15750  cosq34lt1  15764  cos02pilt1  15765  ioocosf1o  15768  gausslemma2dlem1a  15980  2sqlem2  16037  2sqlem3  16039