![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4d | Unicode version |
Description: More general version of 3imtr4i 201. 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 169 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | sylbid 150 |
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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: onsucelsucr 4525 unielrel 5174 ovmpos 6020 caofrss 6131 caoftrn 6132 f1o2ndf1 6253 nnaord 6534 nnmord 6542 oviec 6667 pmss12g 6701 fiss 7006 pm54.43 7219 ltsopi 7349 lttrsr 7791 ltsosr 7793 aptisr 7808 mulextsr1 7810 axpre-mulext 7917 axltwlin 8055 axlttrn 8056 axltadd 8057 axmulgt0 8059 letr 8070 eqord1 8470 remulext1 8586 mulext1 8599 recexap 8640 prodge0 8841 lt2msq 8873 nnge1 8972 zltp1le 9337 uzss 9578 eluzp1m1 9581 xrletr 9838 ixxssixx 9932 zesq 10670 expcanlem 10727 expcan 10728 nn0opthd 10734 maxleast 11254 climshftlemg 11342 dvds1lem 11841 bezoutlemzz 12035 algcvg 12080 eucalgcvga 12090 rpexp12i 12187 crth 12256 pc2dvds 12362 pcmpt 12375 prmpwdvds 12387 1arith 12399 ercpbl 12807 insubm 12937 subginv 13120 rngpropd 13309 dvdsunit 13462 subrgdvds 13582 tgss 14023 neipsm 14114 ssrest 14142 cos11 14734 lgsdir2lem4 14893 m1lgs 14913 |
Copyright terms: Public domain | W3C validator |