![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4d | GIF 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: → wi 4 ↔ wb 105 |
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 4519 unielrel 5168 ovmpos 6012 caofrss 6121 caoftrn 6122 f1o2ndf1 6243 nnaord 6524 nnmord 6532 oviec 6655 pmss12g 6689 fiss 6990 pm54.43 7203 ltsopi 7333 lttrsr 7775 ltsosr 7777 aptisr 7792 mulextsr1 7794 axpre-mulext 7901 axltwlin 8039 axlttrn 8040 axltadd 8041 axmulgt0 8043 letr 8054 eqord1 8454 remulext1 8570 mulext1 8583 recexap 8624 prodge0 8825 lt2msq 8857 nnge1 8956 zltp1le 9321 uzss 9562 eluzp1m1 9565 xrletr 9822 ixxssixx 9916 zesq 10653 expcanlem 10709 expcan 10710 nn0opthd 10716 maxleast 11236 climshftlemg 11324 dvds1lem 11823 bezoutlemzz 12017 algcvg 12062 eucalgcvga 12072 rpexp12i 12169 crth 12238 pc2dvds 12343 pcmpt 12355 prmpwdvds 12367 1arith 12379 ercpbl 12769 insubm 12894 subginv 13073 rngpropd 13207 dvdsunit 13360 subrgdvds 13455 tgss 13859 neipsm 13950 ssrest 13978 cos11 14570 lgsdir2lem4 14728 m1lgs 14748 |
Copyright terms: Public domain | W3C validator |