![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > breq12i | Structured version Unicode version |
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
breq1i.1 |
![]() ![]() ![]() ![]() |
breq12i.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
breq12i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1i.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | breq12i.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | breq12 4406 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | mp2an 672 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-rab 2808 df-v 3080 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-sn 3987 df-pr 3989 df-op 3993 df-br 4402 |
This theorem is referenced by: 3brtr3g 4432 3brtr4g 4433 caovord2 6386 domunfican 7696 ltsonq 9250 ltanq 9252 ltmnq 9253 prlem934 9314 prlem936 9328 ltsosr 9373 ltasr 9379 ltneg 9951 leneg 9954 inelr 10424 lt2sqi 12072 le2sqi 12073 nn0le2msqi 12163 axlowdimlem6 23346 mdsldmd1i 25888 divcnvlin 27544 |
Copyright terms: Public domain | W3C validator |