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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: onsucelsucr 4394 unielrel 5036 ovmpos 5862 caofrss 5974 caoftrn 5975 f1o2ndf1 6093 nnaord 6373 nnmord 6381 oviec 6503 pmss12g 6537 fiss 6833 pm54.43 7014 ltsopi 7096 lttrsr 7538 ltsosr 7540 aptisr 7555 mulextsr1 7557 axpre-mulext 7664 axltwlin 7800 axlttrn 7801 axltadd 7802 axmulgt0 7804 letr 7815 eqord1 8213 remulext1 8329 mulext1 8342 recexap 8382 prodge0 8580 lt2msq 8612 nnge1 8711 zltp1le 9076 uzss 9314 eluzp1m1 9317 xrletr 9559 ixxssixx 9653 zesq 10378 expcanlem 10430 expcan 10431 nn0opthd 10436 maxleast 10953 climshftlemg 11039 efler 11332 dvds1lem 11431 bezoutlemzz 11617 algcvg 11656 eucalgcvga 11666 rpexp12i 11760 crth 11827 tgss 12159 neipsm 12250 ssrest 12278 |
Copyright terms: Public domain | W3C validator |