Theorem 3simpc 998

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
3simpc	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 985	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
2		3simpa 996	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒))
3	1, 2	sylbi 121	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980

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 982

This theorem is referenced by:  simp3  1001  3adant1  1017  3adantl1  1155  3adantr1  1158  eupickb  2126  find  4636  fovcld  6031  fisseneq  7004  eqsupti  7071  divcanap2  8724  diveqap0  8726  divrecap  8732  divcanap3  8742  eliooord  10020  fzrev3  10179  sqdivap  10712  muldvds2  11999  dvdscmul  12000  dvdsmulc  12001  dvdstr  12010  domneq0  13904  znleval2  14286  cncfmptc  14916  cnplimclemr  14989