Theorem simp1bi 1036

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

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

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 1004

This theorem is referenced by:  limord  4490  smores2  6455  smofvon2dm  6457  smofvon  6460  errel  6706  lincmb01cmp  10231  iccf1o  10232  elfznn0  10342  elfzouz  10379  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  sin01gt0  12316  cos01gt0  12317  sin02gt0  12318  eulerthlema  12795  modprm0  12820  gzcn  12938  subgbas  13758  subgrcl  13759  rngabl  13941  srgcmn  13972  ringgrp  14007  subrngrcl  14210  lmodgrp  14301  coseq00topi  15552  coseq0negpitopi  15553  cosq34lt1  15567  cos11  15570  clwwlkbp  16204  clwwlksswrd  16206  nconstwlpolemgt0  16618