Theorem simp2bi 1044

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  0ellim  4545  smodm  6566  erdm  6821  ixpfn  6991  dif1en  7188  eluzelz  9948  lincmble  10424  elfz3nn0  10540  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  sin01gt0  12555  bitsss  12738  gznegcl  13184  gzcjcl  13185  gzaddcl  13186  gzmulcl  13187  gzabssqcl  13190  4sqlem4a  13200  xpsff1o  13730  subgss  14037  rngmgp  14343  srgmgp  14380  ringmgp  14414  lmodring  14741  lmodprop2d  14795  reeff1oleme  16010  cosq14gt0  16071  cosq23lt0  16072  coseq0q4123  16073  coseq00topi  16074  coseq0negpitopi  16075  cosq34lt1  16090  cos02pilt1  16091  ioocosf1o  16094  gausslemma2dlem1a  16394  2sqlem2  16451  2sqlem3  16453