Theorem simp1bi 1036

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

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

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 1004

This theorem is referenced by:  limord  4487  smores2  6451  smofvon2dm  6453  smofvon  6456  errel  6702  lincmb01cmp  10216  iccf1o  10217  elfznn0  10327  elfzouz  10364  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  sin01gt0  12294  cos01gt0  12295  sin02gt0  12296  eulerthlema  12773  modprm0  12798  gzcn  12916  subgbas  13736  subgrcl  13737  rngabl  13919  srgcmn  13950  ringgrp  13985  subrngrcl  14188  lmodgrp  14279  coseq00topi  15530  coseq0negpitopi  15531  cosq34lt1  15545  cos11  15548  clwwlkbp  16164  clwwlksswrd  16166  nconstwlpolemgt0  16546