![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > oveqd | Unicode version |
Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.) |
Ref | Expression |
---|---|
oveq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
oveqd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | oveq 5874 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rex 2461 df-uni 3808 df-br 4001 df-iota 5173 df-fv 5219 df-ov 5871 |
This theorem is referenced by: oveq123d 5889 oveqdr 5896 csbov12g 5907 ovmpodxf 5993 oprssov 6009 ofeq 6078 fnmpoovd 6209 seqeq2 10422 plusffvalg 12660 mgm1 12668 grpidvalg 12671 grpidd 12681 sgrp1 12695 ismndd 12717 issubmnd 12722 mnd1 12724 ismhm 12730 issubm 12740 isgrp 12760 isgrpd2e 12773 grpidd2 12791 grpinvfvalg 12792 grp1 12852 iscmn 12910 iscmnd 12915 dfur2g 12958 issrg 12961 srgcl 12966 srgass 12967 srgideu 12968 issrgid 12977 srgpcomp 12986 srgpcompp 12987 isring 12996 ringcl 13009 crngcom 13010 iscrng2 13011 ringass 13012 ringideu 13013 isringid 13021 ringidss 13025 ringpropd 13030 ring1 13049 opprmulg 13055 oppr0g 13063 oppr1g 13064 opprnegg 13065 mulgass3 13066 reldvdsrsrg 13073 dvdsrvald 13074 dvdsrd 13075 opprunitd 13091 blfvalps 13518 |
Copyright terms: Public domain | W3C validator |