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  2162  find  4720  fovcld  6157  fisseneq  7194  eqsupti  7286  divcanap2  8950  diveqap0  8952  divrecap  8958  divcanap3  8968  eliooord  10257  fzrev3  10417  sqdivap  10961  swrdlend  11343  swrdnd  11344  ccats1pfxeqbi  11427  muldvds2  12496  dvdscmul  12497  dvdsmulc  12498  dvdstr  12507  domneq0  14407  znleval2  14789  cncfmptc  15448  cnplimclemr  15521  uhgr2edg  16188  umgr2edgneu  16194  clwwlknp  16399