Metamath Proof Explorer

Theorem n0lpligALT

Description: Alternate version of n0lplig using the predicate e/ instead of -. e. and whose proof bypasses nsnlplig . (Contributed by AV, 28-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion n0lpligALT G Plig G


Step Hyp Ref Expression
1 eqid G = G
2 1 l2p G Plig G a G b G a b a b
3 noel ¬ a
4 3 pm2.21i a G
5 4 3ad2ant2 a b a b G
6 5 a1i a G b G a b a b G
7 6 rexlimivv a G b G a b a b G
8 2 7 syl G Plig G G
9 simpr G Plig G G
10 8 9 pm2.61danel G Plig G