Metamath Proof Explorer


Theorem 4atexlempw

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

Ref Expression
Hypothesis 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
Assertion 4atexlempw φ P A ¬ P ˙ W

Proof

Step Hyp Ref Expression
1 4thatlem.ph φ K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q
2 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W S A R A ¬ R ˙ W P ˙ R = Q ˙ R T A U ˙ T = V ˙ T P Q ¬ S ˙ P ˙ Q P A ¬ P ˙ W
3 1 2 sylbi φ P A ¬ P ˙ W