![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opeq12i | Unicode version |
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
opeq1i.1 |
![]() ![]() ![]() ![]() |
opeq12i.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
opeq12i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | opeq12i.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | opeq12 3792 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 426 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-v 2751 df-un 3145 df-sn 3610 df-pr 3611 df-op 3613 |
This theorem is referenced by: addpinq1 7476 genipv 7521 ltexpri 7625 recexpr 7650 cauappcvgprlemladdru 7668 cauappcvgprlemladdrl 7669 cauappcvgpr 7674 caucvgprlemcl 7688 caucvgprlemladdrl 7690 caucvgpr 7694 caucvgprprlemval 7700 caucvgprprlemnbj 7705 caucvgprprlemmu 7707 caucvgprprlemclphr 7717 caucvgprprlemaddq 7720 caucvgprprlem1 7721 caucvgprprlem2 7722 caucvgsr 7814 pitonnlem1 7857 axi2m1 7887 axcaucvg 7912 |
Copyright terms: Public domain | W3C validator |