This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psstr

Description: Transitive law for proper subclass. Theorem 9 of Suppes p. 23. (Contributed by NM, 7-Feb-1996)

Ref Expression
Assertion psstr 
|- ( ( A C. B /\ B C. C ) -> A C. C )

Proof

Step Hyp Ref Expression
1 pssss 
 |-  ( A C. B -> A C_ B )
2 pssss 
 |-  ( B C. C -> B C_ C )
3 1 2 sylan9ss 
 |-  ( ( A C. B /\ B C. C ) -> A C_ C )
4 pssn2lp 
 |-  -. ( C C. B /\ B C. C )
5 psseq1 
 |-  ( A = C -> ( A C. B <-> C C. B ) )
6 5 anbi1d 
 |-  ( A = C -> ( ( A C. B /\ B C. C ) <-> ( C C. B /\ B C. C ) ) )
7 4 6 mtbiri 
 |-  ( A = C -> -. ( A C. B /\ B C. C ) )
8 7 con2i 
 |-  ( ( A C. B /\ B C. C ) -> -. A = C )
9 dfpss2 
 |-  ( A C. C <-> ( A C_ C /\ -. A = C ) )
10 3 8 9 sylanbrc 
 |-  ( ( A C. B /\ B C. C ) -> A C. C )