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  4748  fovcld  6196  fisseneq  7247  eqsupti  7343  divcanap2  9019  diveqap0  9021  divrecap  9027  divcanap3  9037  eliooord  10348  fzrev3  10512  sqdivap  11062  swrdlend  11453  swrdnd  11454  ccats1pfxeqbi  11537  muldvds2  12610  dvdscmul  12611  dvdsmulc  12612  dvdstr  12621  rng1zr  14367  srg1zr  14399  domneq0  14691  znleval2  15099  aspid  15127  cncfmptc  15834  cnplimclemr  15907  uhgr2edg  16664  umgr2edgneu  16670  clwwlknp  16875