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  10355  lincmble  10356  iccf1o  10357  elfznn0  10470  elfzouz  10507  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  eulerthlema  12952  modprm0  12977  gzcn  13095  ballotfilemscr  13206  ballotfilemrinv0  13220  subgbas  13979  subgrcl  13980  rngabl  14163  srgcmn  14194  ringgrp  14229  subrngrcl  14434  lmodgrp  14554  coseq00topi  15812  coseq0negpitopi  15813  cosq34lt1  15827  cos11  15830  clwwlkbp  16502  clwwlksswrd  16504  nconstwlpolemgt0  16962