Theorem simp2bi 1015

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

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

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 982

This theorem is referenced by:  0ellim  4434  smodm  6358  erdm  6611  ixpfn  6772  dif1en  6949  eluzelz  9629  elfz3nn0  10209  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  bitsss  12129  gznegcl  12571  gzcjcl  12572  gzaddcl  12573  gzmulcl  12574  gzabssqcl  12577  4sqlem4a  12587  xpsff1o  13053  subgss  13382  rngmgp  13570  srgmgp  13602  ringmgp  13636  lmodring  13929  lmodprop2d  13982  reeff1oleme  15116  cosq14gt0  15176  cosq23lt0  15177  coseq0q4123  15178  coseq00topi  15179  coseq0negpitopi  15180  cosq34lt1  15194  cos02pilt1  15195  ioocosf1o  15198  gausslemma2dlem1a  15407  2sqlem2  15464  2sqlem3  15466