Theorem simp1bi 1012

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

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

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 980

This theorem is referenced by:  limord  4397  smores2  6298  smofvon2dm  6300  smofvon  6303  errel  6547  lincmb01cmp  10006  iccf1o  10007  elfznn0  10117  elfzouz  10154  ef01bndlem  11767  sin01bnd  11768  cos01bnd  11769  sin01gt0  11772  cos01gt0  11773  sin02gt0  11774  eulerthlema  12233  modprm0  12257  gzcn  12373  subgbas  13044  subgrcl  13045  srgcmn  13155  ringgrp  13190  lmodgrp  13390  coseq00topi  14396  coseq0negpitopi  14397  cosq34lt1  14411  cos11  14414  nconstwlpolemgt0  14952