Theorem simp1bi 1014

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

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

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 982

This theorem is referenced by:  limord  4431  smores2  6361  smofvon2dm  6363  smofvon  6366  errel  6610  lincmb01cmp  10097  iccf1o  10098  elfznn0  10208  elfzouz  10245  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  eulerthlema  12425  modprm0  12450  gzcn  12568  subgbas  13386  subgrcl  13387  rngabl  13569  srgcmn  13600  ringgrp  13635  subrngrcl  13837  lmodgrp  13928  coseq00topi  15179  coseq0negpitopi  15180  cosq34lt1  15194  cos11  15197  nconstwlpolemgt0  15821