Theorem simp1bi 1039

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

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

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 1007

This theorem is referenced by:  limord  4515  smores2  6524  smofvon2dm  6526  smofvon  6529  errel  6775  lincmb01cmp  10335  lincmble  10336  iccf1o  10337  elfznn0  10447  elfzouz  10484  ef01bndlem  12438  sin01bnd  12439  cos01bnd  12440  sin01gt0  12444  cos01gt0  12445  sin02gt0  12446  eulerthlema  12923  modprm0  12948  gzcn  13066  subgbas  13887  subgrcl  13888  rngabl  14071  srgcmn  14102  ringgrp  14137  subrngrcl  14340  lmodgrp  14434  coseq00topi  15692  coseq0negpitopi  15693  cosq34lt1  15707  cos11  15710  clwwlkbp  16382  clwwlksswrd  16384  nconstwlpolemgt0  16841