Metamath Proof Explorer

Theorem pssirrOLD

Description: Obsolete version of pssirr as of 10-Jun-2026. (Contributed by NM, 7-Feb-1996) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion pssirrOLD 
|- -. A C. A

Proof

Step Hyp Ref Expression
1 pm3.24 
 |-  -. ( A C_ A /\ -. A C_ A )
2 dfpss3 
 |-  ( A C. A <-> ( A C_ A /\ -. A C_ A ) )
3 1 2 mtbir 
 |-  -. A C. A