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  4521  smores2  6538  smofvon2dm  6540  smofvon  6543  errel  6789  lincmb01cmp  10358  lincmble  10359  iccf1o  10360  elfznn0  10473  elfzouz  10510  ef01bndlem  12471  sin01bnd  12472  cos01bnd  12473  sin01gt0  12477  cos01gt0  12478  sin02gt0  12479  eulerthlema  12956  modprm0  12981  gzcn  13099  ballotfilemscr  13210  ballotfilemrinv0  13224  subgbas  13935  subgrcl  13936  rngabl  14178  srgcmn  14213  ringgrp  14248  subrngrcl  14453  lmodgrp  14572  coseq00topi  15830  coseq0negpitopi  15831  cosq34lt1  15845  cos11  15848  clwwlkbp  16520  clwwlksswrd  16522  nconstwlpolemgt0  16989