Theorem simp1bi 1002

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 999	1 ⊢ (𝜑 → 𝜓)

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

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 970

This theorem is referenced by:  limord  4373  smores2  6262  smofvon2dm  6264  smofvon  6267  errel  6510  lincmb01cmp  9939  iccf1o  9940  elfznn0  10049  elfzouz  10086  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  eulerthlema  12162  modprm0  12186  gzcn  12302  coseq00topi  13396  coseq0negpitopi  13397  cosq34lt1  13411  cos11  13414  nconstwlpolemgt0  13942