Theorem simp1bi 1038

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

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

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 1006

This theorem is referenced by:  limord  4492  smores2  6460  smofvon2dm  6462  smofvon  6465  errel  6711  lincmb01cmp  10238  iccf1o  10239  elfznn0  10349  elfzouz  10386  ef01bndlem  12322  sin01bnd  12323  cos01bnd  12324  sin01gt0  12328  cos01gt0  12329  sin02gt0  12330  eulerthlema  12807  modprm0  12832  gzcn  12950  subgbas  13770  subgrcl  13771  rngabl  13954  srgcmn  13985  ringgrp  14020  subrngrcl  14223  lmodgrp  14314  coseq00topi  15565  coseq0negpitopi  15566  cosq34lt1  15580  cos11  15583  clwwlkbp  16252  clwwlksswrd  16254  nconstwlpolemgt0  16694