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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  limord  4540  smores2  6565  smofvon2dm  6567  smofvon  6570  errel  6816  lincmb01cmp  10407  lincmble  10408  iccf1o  10409  elfznn0  10523  elfzouz  10560  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  sin01gt0  12531  cos01gt0  12532  sin02gt0  12533  eulerthlema  13010  modprm0  13035  gzcn  13153  ballotfilemscr  13264  ballotfilemrinv0  13278  subgbas  13983  subgrcl  13984  rngabl  14236  srgcmn  14272  ringgrp  14307  subrngrcl  14513  lmodgrp  14632  coseq00topi  15939  coseq0negpitopi  15940  cosq34lt1  15954  cos11  15957  clwwlkbp  16648  clwwlksswrd  16650  nconstwlpolemgt0  17126