![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr4d | GIF 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: → wi 4 ↔ wb 104 |
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 4353 unielrel 4992 ovmpt2s 5806 caofrss 5917 caoftrn 5918 f1o2ndf1 6031 nnaord 6308 nnmord 6316 oviec 6438 pmss12g 6472 pm54.43 6915 ltsopi 6976 lttrsr 7405 ltsosr 7407 aptisr 7421 mulextsr1 7423 axpre-mulext 7520 axltwlin 7651 axlttrn 7652 axltadd 7653 axmulgt0 7655 letr 7665 eqord1 8058 remulext1 8173 mulext1 8186 recexap 8219 prodge0 8412 lt2msq 8444 nnge1 8543 zltp1le 8902 uzss 9138 eluzp1m1 9141 xrletr 9374 ixxssixx 9468 zesq 10187 expcanlem 10239 expcan 10240 nn0opthd 10245 maxleast 10761 climshftlemg 10845 efler 11138 dvds1lem 11234 bezoutlemzz 11418 algcvg 11457 eucalgcvga 11467 rpexp12i 11561 crth 11627 tgss 11915 neipsm 12006 ssrest 12034 |
Copyright terms: Public domain | W3C validator |