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  4519  smores2  6527  ersym  6781  ertr  6784  fvixp  6940  en2  7067  fiintim  7193  eluzle  9872  lincmble  10343  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  sin01gt0  12456  gznegcl  13081  gzcjcl  13082  gzaddcl  13083  gzmulcl  13084  gzabssqcl  13087  4sqlem4a  13097  ennnfonelemim  13196  prdsbasprj  13516  xpsff1o  13583  subggrp  13915  srgdilem  14134  srgrz  14149  srglz  14150  ringdilem  14177  ringsrg  14212  subrngss  14368  lmodlema  14489  reeff1oleme  15686  cosq14gt0  15746  cosq23lt0  15747  coseq0q4123  15748  coseq00topi  15749  coseq0negpitopi  15750  cosq34lt1  15764  cos02pilt1  15765  ioocosf1o  15768  2sqlem2  16037  2sqlem3  16039