Metamath Proof Explorer


Theorem 4atexlemp

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 4atexlemp φPA

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 1 4atexlempw φPA¬P˙W
3 2 simpld φPA