Theorem simp2bi 1037

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

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

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 1004

This theorem is referenced by:  0ellim  4489  smodm  6443  erdm  6698  ixpfn  6859  dif1en  7049  eluzelz  9743  elfz3nn0  10323  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  sin01gt0  12289  bitsss  12472  gznegcl  12914  gzcjcl  12915  gzaddcl  12916  gzmulcl  12917  gzabssqcl  12920  4sqlem4a  12930  xpsff1o  13398  subgss  13727  rngmgp  13915  srgmgp  13947  ringmgp  13981  lmodring  14275  lmodprop2d  14328  reeff1oleme  15462  cosq14gt0  15522  cosq23lt0  15523  coseq0q4123  15524  coseq00topi  15525  coseq0negpitopi  15526  cosq34lt1  15540  cos02pilt1  15541  ioocosf1o  15544  gausslemma2dlem1a  15753  2sqlem2  15810  2sqlem3  15812