| 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 191 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
| 4 | 3bitr2d.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: ceqsralt 2830 frecsuclem 6572 indpi 7562 cauappcvgprlemladdru 7876 prsrlt 8007 lesub2 8637 ltsub2 8639 rec11ap 8890 avglt1 9383 rpnegap 9921 modqmuladdnn0 10631 expap0 10832 swrdspsleq 11249 2shfti 11393 mulreap 11426 minmax 11792 lemininf 11796 xrminmax 11827 xrlemininf 11833 modremain 12492 nnwosdc 12612 nn0seqcvgd 12615 divgcdcoprm0 12675 ismgmid 13462 grpsubeq0 13671 grpsubadd 13673 eqg0el 13818 isunitd 14123 lsslss 14398 isridlrng 14499 zndvds 14666 znleval 14670 isxmet2d 15075 xblss2 15132 neibl 15218 ellimc3apf 15387 logbgt0b 15693 lgsne0 15770 lgsabs1 15771 lgsquadlem1 15809 m1lgs 15817 eupth2lem2dc 16313 eupth2lem3lem4fi 16327 iswomninnlem 16674 |
| Copyright terms: Public domain | W3C validator |