Theorem simp2bi 1037

Description: Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
3simp1bi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
simp2bi	⊢ (𝜑 → 𝜒)

Proof of Theorem simp2bi

Step	Hyp	Ref	Expression
1		3simp1bi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
2	1	biimpi 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
3	2	simp2d 1034	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

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

This theorem is referenced by:  0ellim  4489  smodm  6443  erdm  6698  ixpfn  6859  dif1en  7049  eluzelz  9739  elfz3nn0  10319  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  sin01gt0  12281  bitsss  12464  gznegcl  12906  gzcjcl  12907  gzaddcl  12908  gzmulcl  12909  gzabssqcl  12912  4sqlem4a  12922  xpsff1o  13390  subgss  13719  rngmgp  13907  srgmgp  13939  ringmgp  13973  lmodring  14267  lmodprop2d  14320  reeff1oleme  15454  cosq14gt0  15514  cosq23lt0  15515  coseq0q4123  15516  coseq00topi  15517  coseq0negpitopi  15518  cosq34lt1  15532  cos02pilt1  15533  ioocosf1o  15536  gausslemma2dlem1a  15745  2sqlem2  15802  2sqlem3  15804