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  4524  smodm  6535  erdm  6790  ixpfn  6952  dif1en  7149  eluzelz  9884  lincmble  10359  elfz3nn0  10474  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  sin01gt0  12476  bitsss  12659  gznegcl  13101  gzcjcl  13102  gzaddcl  13103  gzmulcl  13104  gzabssqcl  13107  4sqlem4a  13117  xpsff1o  13616  subgss  13930  rngmgp  14178  srgmgp  14214  ringmgp  14248  lmodring  14572  lmodprop2d  14625  reeff1oleme  15766  cosq14gt0  15826  cosq23lt0  15827  coseq0q4123  15828  coseq00topi  15829  coseq0negpitopi  15830  cosq34lt1  15844  cos02pilt1  15845  ioocosf1o  15848  gausslemma2dlem1a  16060  2sqlem2  16117  2sqlem3  16119