Theorem 3simpc 1027

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

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

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 1011

This theorem is referenced by:  simp3  1030  3adant1  1046  3adantl1  1184  3adantr1  1187  eupickb  2168  find  4744  fovcld  6187  fisseneq  7236  eqsupti  7330  divcanap2  9004  diveqap0  9006  divrecap  9012  divcanap3  9022  eliooord  10313  fzrev3  10477  sqdivap  11023  swrdlend  11413  swrdnd  11414  ccats1pfxeqbi  11497  muldvds2  12567  dvdscmul  12568  dvdsmulc  12569  dvdstr  12578  rng1zr  14242  srg1zr  14274  domneq0  14564  znleval2  14972  aspid  15000  cncfmptc  15680  cnplimclemr  15753  uhgr2edg  16430  umgr2edgneu  16436  clwwlknp  16641