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  4486  smores2  6446  smofvon2dm  6448  smofvon  6451  errel  6697  lincmb01cmp  10207  iccf1o  10208  elfznn0  10318  elfzouz  10355  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  eulerthlema  12760  modprm0  12785  gzcn  12903  subgbas  13723  subgrcl  13724  rngabl  13906  srgcmn  13937  ringgrp  13972  subrngrcl  14175  lmodgrp  14266  coseq00topi  15517  coseq0negpitopi  15518  cosq34lt1  15532  cos11  15535  nconstwlpolemgt0  16462