Theorem 3simpc 999

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 986	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
2		3simpa 997	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → (𝜓 ∧ 𝜒))
3	1, 2	sylbi 121	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

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

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 983

This theorem is referenced by:  simp3  1002  3adant1  1018  3adantl1  1156  3adantr1  1159  eupickb  2136  find  4651  fovcld  6057  fisseneq  7038  eqsupti  7105  divcanap2  8760  diveqap0  8762  divrecap  8768  divcanap3  8778  eliooord  10057  fzrev3  10216  sqdivap  10755  swrdlend  11119  swrdnd  11120  muldvds2  12172  dvdscmul  12173  dvdsmulc  12174  dvdstr  12183  domneq0  14078  znleval2  14460  cncfmptc  15112  cnplimclemr  15185