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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp3  1030  3adant1  1046  3adantl1  1184  3adantr1  1187  eupickb  2168  find  4746  fovcld  6193  fisseneq  7242  eqsupti  7336  divcanap2  9011  diveqap0  9013  divrecap  9019  divcanap3  9029  eliooord  10332  fzrev3  10496  sqdivap  11042  swrdlend  11432  swrdnd  11433  ccats1pfxeqbi  11516  muldvds2  12586  dvdscmul  12587  dvdsmulc  12588  dvdstr  12597  rng1zr  14261  srg1zr  14293  domneq0  14583  znleval2  14991  aspid  15019  cncfmptc  15699  cnplimclemr  15772  uhgr2edg  16459  umgr2edgneu  16465  clwwlknp  16670