Metamath Proof Explorer


Theorem sucdomOLD

Description: Obsolete version of sucdom as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sucdomOLD A ω A B suc A B

Proof

Step Hyp Ref Expression
1 sucdom2 A B suc A B
2 php4 A ω A suc A
3 sdomdomtr A suc A suc A B A B
4 3 ex A suc A suc A B A B
5 2 4 syl A ω suc A B A B
6 1 5 impbid2 A ω A B suc A B