Metamath Proof Explorer


Theorem 4atexlemnslpq

Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)

Ref Expression
Hypothesis 4thatlem.ph φKHLWHPA¬P˙WQA¬Q˙WSARA¬R˙WP˙R=Q˙RTAU˙T=V˙TPQ¬S˙P˙Q
Assertion 4atexlemnslpq φ¬S˙P˙Q

Proof

Step Hyp Ref Expression
1 4thatlem.ph φKHLWHPA¬P˙WQA¬Q˙WSARA¬R˙WP˙R=Q˙RTAU˙T=V˙TPQ¬S˙P˙Q
2 simp3r KHLWHPA¬P˙WQA¬Q˙WSARA¬R˙WP˙R=Q˙RTAU˙T=V˙TPQ¬S˙P˙Q¬S˙P˙Q
3 1 2 sylbi φ¬S˙P˙Q