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  4430  smores2  6352  smofvon2dm  6354  smofvon  6357  errel  6601  lincmb01cmp  10078  iccf1o  10079  elfznn0  10189  elfzouz  10226  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  eulerthlema  12398  modprm0  12423  gzcn  12541  subgbas  13308  subgrcl  13309  rngabl  13491  srgcmn  13522  ringgrp  13557  subrngrcl  13759  lmodgrp  13850  coseq00topi  15071  coseq0negpitopi  15072  cosq34lt1  15086  cos11  15089  nconstwlpolemgt0  15708