Theorem 3simpc 1023

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

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

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 1007

This theorem is referenced by:  simp3  1026  3adant1  1042  3adantl1  1180  3adantr1  1183  eupickb  2164  find  4726  fovcld  6166  fisseneq  7208  eqsupti  7300  divcanap2  8974  diveqap0  8976  divrecap  8982  divcanap3  8992  eliooord  10283  fzrev3  10446  sqdivap  10992  swrdlend  11378  swrdnd  11379  ccats1pfxeqbi  11462  muldvds2  12531  dvdscmul  12532  dvdsmulc  12533  dvdstr  12542  rng1zr  14202  srg1zr  14233  domneq0  14522  znleval2  14931  cncfmptc  15590  cnplimclemr  15663  uhgr2edg  16330  umgr2edgneu  16336  clwwlknp  16541