Theorem simp3bi 1038

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 1035	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  ax-ia2 107  ax-ia3 108

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

This theorem is referenced by:  limuni  4491  smores2  6455  ersym  6709  ertr  6712  fvixp  6867  en2  6993  fiintim  7118  eluzle  9761  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  sin01gt0  12316  gznegcl  12941  gzcjcl  12942  gzaddcl  12943  gzmulcl  12944  gzabssqcl  12947  4sqlem4a  12957  ennnfonelemim  13038  prdsbasprj  13358  xpsff1o  13425  subggrp  13757  srgdilem  13975  srgrz  13990  srglz  13991  ringdilem  14018  ringsrg  14053  subrngss  14207  lmodlema  14299  reeff1oleme  15489  cosq14gt0  15549  cosq23lt0  15550  coseq0q4123  15551  coseq00topi  15552  coseq0negpitopi  15553  cosq34lt1  15567  cos02pilt1  15568  ioocosf1o  15571  2sqlem2  15837  2sqlem3  15839