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  4542  smores2  6569  smofvon2dm  6571  smofvon  6574  errel  6820  lincmb01cmp  10423  lincmble  10424  iccf1o  10425  elfznn0  10539  elfzouz  10576  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  eulerthlema  13038  modprm0  13063  gzcn  13181  ballotfilemscr  13321  ballotfilemrinv0  13335  subgbas  14041  subgrcl  14042  rngabl  14342  srgcmn  14378  ringgrp  14413  subrngrcl  14621  lmodgrp  14740  coseq00topi  16074  coseq0negpitopi  16075  cosq34lt1  16090  cos11  16093  clwwlkbp  16853  clwwlksswrd  16855  nconstwlpolemgt0  17333