Theorem simp1bi 996

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp1bi	⊢ (𝜑 → 𝜓)

Proof of Theorem simp1bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 119	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 993	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  limord  4317  smores2  6191  smofvon2dm  6193  smofvon  6196  errel  6438  lincmb01cmp  9789  iccf1o  9790  elfznn0  9897  elfzouz  9931  ef01bndlem  11466  sin01bnd  11467  cos01bnd  11468  sin01gt0  11471  cos01gt0  11472  sin02gt0  11473  coseq00topi  12919  coseq0negpitopi  12920  cosq34lt1  12934