Theorem simp1bi 1012

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 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp1d 1009	1 ⊢ (𝜑 → 𝜓)

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

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  limord  4389  smores2  6285  smofvon2dm  6287  smofvon  6290  errel  6534  lincmb01cmp  9974  iccf1o  9975  elfznn0  10084  elfzouz  10121  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  sin01gt0  11737  cos01gt0  11738  sin02gt0  11739  eulerthlema  12197  modprm0  12221  gzcn  12337  srgcmn  12955  ringgrp  12990  coseq00topi  13836  coseq0negpitopi  13837  cosq34lt1  13851  cos11  13854  nconstwlpolemgt0  14381