![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4d | Unicode version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr4d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3eqtr4d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3eqtr4d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3eqtr4d.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 3eqtr4d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqtr4d 2072 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqtr4d 2072 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: fnsnfv 5175 fvco2 5185 resfunexg 5325 fcof1 5366 fliftfun 5379 caovdir2d 5619 caov32d 5623 caov31d 5625 caov4d 5627 caovlem2d 5635 caofcom 5676 cnvf1olem 5787 tfrlem1 5864 tfrlemisucaccv 5880 frecrdg 5931 oav2 5982 omv2 5984 omsuc 5990 nnmsucr 6006 ecovicom 6150 ecoviass 6152 ecovidi 6154 addcompig 6313 addasspig 6314 mulcompig 6315 mulasspig 6316 distrpig 6317 addassnqg 6366 addnq0mo 6430 mulnq0mo 6431 nqnq0a 6437 nqnq0m 6438 distrnq0 6442 mulcomnq0 6443 addassnq0 6445 addcmpblnr 6667 mulcmpblnrlemg 6668 addsrmo 6671 mulsrmo 6672 ltsrprg 6675 recexgt0sr 6701 mulgt0sr 6704 mulextsr1lem 6706 addcnsrec 6739 mulcnsrec 6740 pitonnlem2 6743 axaddcom 6754 adddir 6816 mul32 6940 mul31 6941 add32 6967 add4 6969 sub32 7041 sub4 7052 subdir 7179 mulneg2 7189 mulreim 7388 apadd1 7392 apneg 7395 divassap 7451 divdirap 7456 divmul13ap 7473 divmul24ap 7474 divdiv32ap 7478 conjmulap 7487 zeo 8119 lincmb01cmp 8641 iccf1o 8642 expp1 8916 expnegap0 8917 expaddzaplem 8952 expaddzap 8953 expmulzap 8955 sqneg 8967 sqdivap 8972 subsq2 9012 binom2 9015 crre 9085 remim 9088 mulreap 9092 reneg 9096 readd 9097 remullem 9099 redivap 9102 imneg 9104 imadd 9105 imdivap 9109 cjcj 9111 cjadd 9112 cjmulrcl 9115 cjneg 9118 imval2 9122 absneg 9219 |
Copyright terms: Public domain | W3C validator |