Theorem simp3bi 1041

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp3bi	⊢ (𝜑 → 𝜃)

Proof of Theorem simp3bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp3d 1038	1 ⊢ (𝜑 → 𝜃)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  limuni  4522  smores2  6538  ersym  6792  ertr  6795  fvixp  6951  en2  7078  fiintim  7204  eluzle  9887  lincmble  10359  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  sin01gt0  12476  gznegcl  13101  gzcjcl  13102  gzaddcl  13103  gzmulcl  13104  gzabssqcl  13107  4sqlem4a  13117  ennnfonelemim  13262  xpsff1o  13616  subggrp  13933  prdsbasprj  14127  srgdilem  14215  srgrz  14230  srglz  14231  ringdilem  14258  ringsrg  14293  subrngss  14449  lmodlema  14569  reeff1oleme  15766  cosq14gt0  15826  cosq23lt0  15827  coseq0q4123  15828  coseq00topi  15829  coseq0negpitopi  15830  cosq34lt1  15844  cos02pilt1  15845  ioocosf1o  15848  2sqlem2  16117  2sqlem3  16119