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  4498  smores2  6503  smofvon2dm  6505  smofvon  6508  errel  6754  lincmb01cmp  10281  iccf1o  10282  elfznn0  10392  elfzouz  10429  ef01bndlem  12378  sin01bnd  12379  cos01bnd  12380  sin01gt0  12384  cos01gt0  12385  sin02gt0  12386  eulerthlema  12863  modprm0  12888  gzcn  13006  subgbas  13826  subgrcl  13827  rngabl  14010  srgcmn  14041  ringgrp  14076  subrngrcl  14279  lmodgrp  14370  coseq00topi  15626  coseq0negpitopi  15627  cosq34lt1  15641  cos11  15644  clwwlkbp  16316  clwwlksswrd  16318  nconstwlpolemgt0  16777