![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3imtr3d | GIF version |
Description: More general version of 3imtr3i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.) |
Ref | Expression |
---|---|
3imtr3d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
3imtr3d.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
3imtr3d.3 | ⊢ (𝜑 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
3imtr3d | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imtr3d.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
2 | 3imtr3d.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 3imtr3d.3 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
4 | 2, 3 | sylibd 149 | . 2 ⊢ (𝜑 → (𝜓 → 𝜏)) |
5 | 1, 4 | sylbird 170 | 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: f1imass 5796 focdmex 6140 tposfn2 6291 eroveu 6652 ismkvnex 7183 indpi 7371 axcaucvglemres 7928 qsqeqor 10662 caucvgrelemcau 11021 m1dvdsndvds 12280 pcpremul 12325 pcaddlem 12371 pockthlem 12388 issgrpd 12875 ghmf1 13212 islssmd 13675 limccnpcntop 14601 sincosq1sgn 14704 sincosq2sgn 14705 lgseisenlem2 14909 subctctexmid 15209 neap0mkv 15276 |
Copyright terms: Public domain | W3C validator |