![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitr3d | GIF version |
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
Ref | Expression |
---|---|
3bitr3d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr3d.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
3bitr3d.3 | ⊢ (𝜑 → (𝜒 ↔ 𝜏)) |
Ref | Expression |
---|---|
3bitr3d | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3d.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | |
2 | 3bitr3d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr3d 190 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒)) |
4 | 3bitr3d.3 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 188 | 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: csbcomg 3081 eloprabga 5962 ereldm 6578 mapen 6846 ordiso2 7034 subcan 8212 conjmulap 8686 ltrec 8840 divelunit 10002 fseq1m1p1 10095 fzm1 10100 qsqeqor 10631 fihashneq0 10774 hashfacen 10816 cvg1nlemcau 10993 lenegsq 11104 dvdsmod 11868 bezoutlemle 12009 rpexp 12153 qnumdenbi 12192 eulerthlemh 12231 odzdvds 12245 pcelnn 12320 grpidpropdg 12793 mndpropd 12841 mhmpropd 12857 grppropd 12893 cmnpropd 13098 ringpropd 13217 dvdsrpropdg 13316 lmodprop2d 13438 bdxmet 14004 txmetcnp 14021 cnmet 14033 lgsne0 14442 lgsabs1 14443 |
Copyright terms: Public domain | W3C validator |