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  4483  smores2  6430  smofvon2dm  6432  smofvon  6435  errel  6679  lincmb01cmp  10187  iccf1o  10188  elfznn0  10298  elfzouz  10335  ef01bndlem  12253  sin01bnd  12254  cos01bnd  12255  sin01gt0  12259  cos01gt0  12260  sin02gt0  12261  eulerthlema  12738  modprm0  12763  gzcn  12881  subgbas  13701  subgrcl  13702  rngabl  13884  srgcmn  13915  ringgrp  13950  subrngrcl  14152  lmodgrp  14243  coseq00topi  15494  coseq0negpitopi  15495  cosq34lt1  15509  cos11  15512  nconstwlpolemgt0  16363