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  4541  smores2  6565  ersym  6819  ertr  6822  fvixp  6985  en2  7112  fiintim  7238  eluzle  9936  lincmble  10408  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  sin01gt0  12531  gznegcl  13156  gzcjcl  13157  gzaddcl  13158  gzmulcl  13159  gzabssqcl  13162  4sqlem4a  13172  ennnfonelemim  13317  xpsff1o  13672  subggrp  13982  prdsbasprj  14184  srgdilem  14275  srgrz  14290  srglz  14291  ringdilem  14318  ringsrg  14354  subrngss  14510  lmodlema  14630  reeff1oleme  15875  cosq14gt0  15936  cosq23lt0  15937  coseq0q4123  15938  coseq00topi  15939  coseq0negpitopi  15940  cosq34lt1  15954  cos02pilt1  15955  ioocosf1o  15958  2sqlem2  16246  2sqlem3  16248