Theorem simp3bi 1040

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

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

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 1006

This theorem is referenced by:  limuni  4493  smores2  6460  ersym  6714  ertr  6717  fvixp  6872  en2  6998  fiintim  7123  eluzle  9768  ef01bndlem  12319  sin01bnd  12320  cos01bnd  12321  sin01gt0  12325  gznegcl  12950  gzcjcl  12951  gzaddcl  12952  gzmulcl  12953  gzabssqcl  12956  4sqlem4a  12966  ennnfonelemim  13047  prdsbasprj  13367  xpsff1o  13434  subggrp  13766  srgdilem  13985  srgrz  14000  srglz  14001  ringdilem  14028  ringsrg  14063  subrngss  14217  lmodlema  14309  reeff1oleme  15499  cosq14gt0  15559  cosq23lt0  15560  coseq0q4123  15561  coseq00topi  15562  coseq0negpitopi  15563  cosq34lt1  15577  cos02pilt1  15578  ioocosf1o  15581  2sqlem2  15847  2sqlem3  15849