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 4492 unielrel 5138 ovmpos 5976 caofrss 6085 caoftrn 6086 f1o2ndf1 6207 nnaord 6488 nnmord 6496 oviec 6619 pmss12g 6653 fiss 6954 pm54.43 7167 ltsopi 7282 lttrsr 7724 ltsosr 7726 aptisr 7741 mulextsr1 7743 axpre-mulext 7850 axltwlin 7987 axlttrn 7988 axltadd 7989 axmulgt0 7991 letr 8002 eqord1 8402 remulext1 8518 mulext1 8531 recexap 8571 prodge0 8770 lt2msq 8802 nnge1 8901 zltp1le 9266 uzss 9507 eluzp1m1 9510 xrletr 9765 ixxssixx 9859 zesq 10594 expcanlem 10649 expcan 10650 nn0opthd 10656 maxleast 11177 climshftlemg 11265 dvds1lem 11764 bezoutlemzz 11957 algcvg 12002 eucalgcvga 12012 rpexp12i 12109 crth 12178 pc2dvds 12283 pcmpt 12295 prmpwdvds 12307 1arith 12319 insubm 12703 tgss 12857 neipsm 12948 ssrest 12976 cos11 13568 lgsdir2lem4 13726 |
Copyright terms: Public domain | W3C validator |