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  4723  fovcld  6160  fisseneq  7197  eqsupti  7289  divcanap2  8959  diveqap0  8961  divrecap  8967  divcanap3  8977  eliooord  10267  fzrev3  10428  sqdivap  10972  swrdlend  11358  swrdnd  11359  ccats1pfxeqbi  11442  muldvds2  12511  dvdscmul  12512  dvdsmulc  12513  dvdstr  12522  domneq0  14441  znleval2  14851  cncfmptc  15510  cnplimclemr  15583  uhgr2edg  16250  umgr2edgneu  16256  clwwlknp  16461