Metamath Proof Explorer


Theorem nel2nelini

Description: Membership in an intersection implies membership in the second set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis nel2nelini.1 ¬ A C
Assertion nel2nelini ¬ A B C

Proof

Step Hyp Ref Expression
1 nel2nelini.1 ¬ A C
2 nel2nelin ¬ A C ¬ A B C
3 1 2 ax-mp ¬ A B C