Theorem simp3bi 1045

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  limuni  4543  smores2  6569  ersym  6823  ertr  6826  fvixp  6990  en2  7117  fiintim  7243  eluzle  9951  lincmble  10424  ef01bndlem  12549  sin01bnd  12550  cos01bnd  12551  sin01gt0  12555  gznegcl  13184  gzcjcl  13185  gzaddcl  13186  gzmulcl  13187  gzabssqcl  13190  4sqlem4a  13200  ennnfonelemim  13374  xpsff1o  13730  subggrp  14040  prdsbasprj  14290  srgdilem  14381  srgrz  14396  srglz  14397  ringdilem  14424  ringsrg  14460  subrngss  14618  lmodlema  14738  reeff1oleme  16010  cosq14gt0  16071  cosq23lt0  16072  coseq0q4123  16073  coseq00topi  16074  coseq0negpitopi  16075  cosq34lt1  16090  cos02pilt1  16091  ioocosf1o  16094  2sqlem2  16451  2sqlem3  16453