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 2757 frecsuclem 6385 indpi 7304 cauappcvgprlemladdru 7618 prsrlt 7749 lesub2 8376 ltsub2 8378 rec11ap 8627 avglt1 9116 rpnegap 9643 modqmuladdnn0 10324 expap0 10506 2shfti 10795 mulreap 10828 minmax 11193 lemininf 11197 xrminmax 11228 xrlemininf 11234 modremain 11888 nn0seqcvgd 11995 divgcdcoprm0 12055 ismgmid 12631 isxmet2d 13142 xblss2 13199 neibl 13285 ellimc3apf 13423 logbgt0b 13678 lgsne0 13733 lgsabs1 13734 iswomninnlem 14081 |
Copyright terms: Public domain | W3C validator |