Metamath Proof Explorer


Theorem 4atexlemt

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 4atexlemt φTA

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 simp23l KHLWHPA¬P˙WQA¬Q˙WSARA¬R˙WP˙R=Q˙RTAU˙T=V˙TPQ¬S˙P˙QTA
3 1 2 sylbi φTA