Theorem simp3bi 1014

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 1011	1 ⊢ (𝜑 → 𝜃)

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

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 980

This theorem is referenced by:  limuni  4398  smores2  6297  ersym  6549  ertr  6552  fvixp  6705  fiintim  6930  eluzle  9542  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  gznegcl  12375  gzcjcl  12376  gzaddcl  12377  gzmulcl  12378  gzabssqcl  12381  4sqlem4a  12391  ennnfonelemim  12427  xpsff1o  12773  subggrp  13042  srgdilem  13157  srgrz  13172  srglz  13173  ringdilem  13200  ringsrg  13229  lmodlema  13387  reeff1oleme  14232  cosq14gt0  14292  cosq23lt0  14293  coseq0q4123  14294  coseq00topi  14295  coseq0negpitopi  14296  cosq34lt1  14310  cos02pilt1  14311  ioocosf1o  14314  2sqlem2  14501  2sqlem3  14503