Theorem 3simpc 1001

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

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

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 985

This theorem is referenced by:  simp3  1004  3adant1  1020  3adantl1  1158  3adantr1  1161  eupickb  2139  find  4668  fovcld  6080  fisseneq  7064  eqsupti  7131  divcanap2  8795  diveqap0  8797  divrecap  8803  divcanap3  8813  eliooord  10092  fzrev3  10251  sqdivap  10792  swrdlend  11156  swrdnd  11157  ccats1pfxeqbi  11240  muldvds2  12294  dvdscmul  12295  dvdsmulc  12296  dvdstr  12305  domneq0  14201  znleval2  14583  cncfmptc  15235  cnplimclemr  15308  uhgr2edg  15969  umgr2edgneu  15975