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  10416  lincmble  10417  iccf1o  10418  elfznn0  10532  elfzouz  10569  ef01bndlem  12541  sin01bnd  12542  cos01bnd  12543  sin01gt0  12547  cos01gt0  12548  sin02gt0  12549  eulerthlema  13030  modprm0  13055  gzcn  13173  ballotfilemscr  13313  ballotfilemrinv0  13327  subgbas  14032  subgrcl  14033  rngabl  14285  srgcmn  14321  ringgrp  14356  subrngrcl  14562  lmodgrp  14681  coseq00topi  15989  coseq0negpitopi  15990  cosq34lt1  16004  cos11  16007  clwwlkbp  16758  clwwlksswrd  16760  nconstwlpolemgt0  17236