Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  posng Unicode version

Theorem posng 4412
 Description: Partial ordering of a singleton. (Contributed by Jim Kingdon, 5-Dec-2018.)
Assertion
Ref Expression
posng

Proof of Theorem posng
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-po 4033 . 2
2 breq2 3768 . . . . . . . . . . 11
32anbi2d 437 . . . . . . . . . 10
4 breq2 3768 . . . . . . . . . 10
53, 4imbi12d 223 . . . . . . . . 9
65anbi2d 437 . . . . . . . 8
76ralsng 3411 . . . . . . 7
87ralbidv 2326 . . . . . 6
9 simpl 102 . . . . . . . . . 10
10 breq2 3768 . . . . . . . . . 10
119, 10syl5ib 143 . . . . . . . . 9
1211biantrud 288 . . . . . . . 8
1312bicomd 129 . . . . . . 7
1413ralsng 3411 . . . . . 6
158, 14bitrd 177 . . . . 5
1615ralbidv 2326 . . . 4
17 breq12 3769 . . . . . . 7
1817anidms 377 . . . . . 6
1918notbid 592 . . . . 5
2019ralsng 3411 . . . 4
2116, 20bitrd 177 . . 3