![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4d | Unicode version |
Description: More general version of 3imtr4i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.) |
Ref | Expression |
---|---|
3imtr4d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3imtr4d.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3imtr4d.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3imtr4d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr4d.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3imtr4d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 3imtr4d.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylibrd 168 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylbid 149 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: onsucelsucr 4362 unielrel 5002 ovmpos 5826 caofrss 5937 caoftrn 5938 f1o2ndf1 6055 nnaord 6335 nnmord 6343 oviec 6465 pmss12g 6499 pm54.43 6957 ltsopi 7029 lttrsr 7458 ltsosr 7460 aptisr 7474 mulextsr1 7476 axpre-mulext 7573 axltwlin 7704 axlttrn 7705 axltadd 7706 axmulgt0 7708 letr 7718 eqord1 8112 remulext1 8227 mulext1 8240 recexap 8275 prodge0 8470 lt2msq 8502 nnge1 8601 zltp1le 8960 uzss 9196 eluzp1m1 9199 xrletr 9432 ixxssixx 9526 zesq 10251 expcanlem 10303 expcan 10304 nn0opthd 10309 maxleast 10825 climshftlemg 10910 efler 11203 dvds1lem 11299 bezoutlemzz 11483 algcvg 11522 eucalgcvga 11532 rpexp12i 11626 crth 11692 tgss 12014 neipsm 12105 ssrest 12133 |
Copyright terms: Public domain | W3C validator |