Theorem simp1bi 1043

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

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

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 1011

This theorem is referenced by:  limord  4538  smores2  6559  smofvon2dm  6561  smofvon  6564  errel  6810  lincmb01cmp  10388  lincmble  10389  iccf1o  10390  elfznn0  10504  elfzouz  10541  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  eulerthlema  12991  modprm0  13016  gzcn  13134  ballotfilemscr  13245  ballotfilemrinv0  13259  subgbas  13964  subgrcl  13965  rngabl  14217  srgcmn  14253  ringgrp  14288  subrngrcl  14494  lmodgrp  14613  coseq00topi  15919  coseq0negpitopi  15920  cosq34lt1  15934  cos11  15937  clwwlkbp  16619  clwwlksswrd  16621  nconstwlpolemgt0  17088