![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > equequ2 | Structured version Visualization version Unicode version |
Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) |
Ref | Expression |
---|---|
equequ2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ1 1867 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | equcom 1862 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | equcom 1862 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3bitr3g 291 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 |
This theorem is referenced by: ax12v 1934 axc11nlem 2021 axc9lem1 2093 axc9lem2 2133 axc9lem2OLD 2134 axc11nlemALT 2142 dveeq2ALT 2174 ax12v2 2175 equvini 2179 sbequi 2204 eujust 2301 eujustALT 2302 euequ1 2305 euf 2307 mo2 2308 disjxun 4400 axrep2 4517 dtru 4594 zfpair 4637 dfid3 4750 isso2i 4787 iotaval 5557 dff13f 6160 dfwe2 6608 aceq0 8549 zfac 8890 axpowndlem4 9025 zfcndac 9044 injresinj 12025 infpn2 14857 ramub1lem2 14985 fullestrcsetc 16036 fullsetcestrc 16051 symgextf1 17062 mplcoe1 18689 evlslem2 18735 mamulid 19466 mamurid 19467 mdetdiagid 19625 dscmet 21587 lgseisenlem2 24278 dchrisumlem3 24329 usgrasscusgra 25211 bj-ssbequ 31242 bj-ssblem1 31243 bj-ssblem2 31244 bj-ssb1a 31245 bj-ssb1 31246 bj-ssbcom3lem 31263 bj-axc11nlemv 31347 bj-axc15v 31362 bj-axrep2 31404 bj-dtru 31412 bj-eleq1w 31455 bj-ax8 31495 wl-aleq 31868 wl-mo2df 31899 wl-eudf 31901 wl-euequ1f 31903 wl-mo2t 31904 wl-ax12v2 31909 wl-ax12v3 31912 dveeq2-o 32504 axc11n-16 32509 ax12eq 32512 ax12inda 32519 ax12v2-o 32520 fphpd 35659 iotavalb 36781 |
Copyright terms: Public domain | W3C validator |