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  4543  smodm  6562  erdm  6817  ixpfn  6986  dif1en  7183  eluzelz  9933  lincmble  10408  elfz3nn0  10524  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  sin01gt0  12531  bitsss  12714  gznegcl  13156  gzcjcl  13157  gzaddcl  13158  gzmulcl  13159  gzabssqcl  13162  4sqlem4a  13172  xpsff1o  13672  subgss  13979  rngmgp  14237  srgmgp  14274  ringmgp  14308  lmodring  14633  lmodprop2d  14687  reeff1oleme  15875  cosq14gt0  15936  cosq23lt0  15937  coseq0q4123  15938  coseq00topi  15939  coseq0negpitopi  15940  cosq34lt1  15954  cos02pilt1  15955  ioocosf1o  15958  gausslemma2dlem1a  16189  2sqlem2  16246  2sqlem3  16248