Theorem simp1bi 1015

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

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

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 983

This theorem is referenced by:  limord  4447  smores2  6390  smofvon2dm  6392  smofvon  6395  errel  6639  lincmb01cmp  10138  iccf1o  10139  elfznn0  10249  elfzouz  10286  ef01bndlem  12117  sin01bnd  12118  cos01bnd  12119  sin01gt0  12123  cos01gt0  12124  sin02gt0  12125  eulerthlema  12602  modprm0  12627  gzcn  12745  subgbas  13564  subgrcl  13565  rngabl  13747  srgcmn  13778  ringgrp  13813  subrngrcl  14015  lmodgrp  14106  coseq00topi  15357  coseq0negpitopi  15358  cosq34lt1  15372  cos11  15375  nconstwlpolemgt0  16118