Theorem simp3bi 1017

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

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

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 983

This theorem is referenced by:  limuni  4447  smores2  6387  ersym  6639  ertr  6642  fvixp  6797  en2  6919  fiintim  7035  eluzle  9667  ef01bndlem  12111  sin01bnd  12112  cos01bnd  12113  sin01gt0  12117  gznegcl  12742  gzcjcl  12743  gzaddcl  12744  gzmulcl  12745  gzabssqcl  12748  4sqlem4a  12758  ennnfonelemim  12839  prdsbasprj  13158  xpsff1o  13225  subggrp  13557  srgdilem  13775  srgrz  13790  srglz  13791  ringdilem  13818  ringsrg  13853  subrngss  14006  lmodlema  14098  reeff1oleme  15288  cosq14gt0  15348  cosq23lt0  15349  coseq0q4123  15350  coseq00topi  15351  coseq0negpitopi  15352  cosq34lt1  15366  cos02pilt1  15367  ioocosf1o  15370  2sqlem2  15636  2sqlem3  15638