Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr2d | GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr2d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr2d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
3bitr2d.3 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
3bitr2d | ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr2d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 3bitr2d.2 | . . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) | |
3 | 1, 2 | bitr4d 190 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3bitr2d.3 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 187 | 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: ceqsralt 2739 frecsuclem 6353 indpi 7262 cauappcvgprlemladdru 7576 prsrlt 7707 lesub2 8332 ltsub2 8334 rec11ap 8583 avglt1 9071 rpnegap 9593 modqmuladdnn0 10267 expap0 10449 2shfti 10731 mulreap 10764 minmax 11129 lemininf 11133 xrminmax 11162 xrlemininf 11168 modremain 11819 nn0seqcvgd 11917 divgcdcoprm0 11977 isxmet2d 12748 xblss2 12805 neibl 12891 ellimc3apf 13029 logbgt0b 13283 iswomninnlem 13620 |
Copyright terms: Public domain | W3C validator |