![]() |
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 2779 frecsuclem 6432 indpi 7372 cauappcvgprlemladdru 7686 prsrlt 7817 lesub2 8445 ltsub2 8447 rec11ap 8698 avglt1 9188 rpnegap 9718 modqmuladdnn0 10401 expap0 10584 2shfti 10875 mulreap 10908 minmax 11273 lemininf 11277 xrminmax 11308 xrlemininf 11314 modremain 11969 nnwosdc 12075 nn0seqcvgd 12076 divgcdcoprm0 12136 ismgmid 12856 grpsubeq0 13045 grpsubadd 13047 eqg0el 13185 isunitd 13473 lsslss 13714 isridlrng 13815 isxmet2d 14325 xblss2 14382 neibl 14468 ellimc3apf 14606 logbgt0b 14861 lgsne0 14917 lgsabs1 14918 m1lgs 14930 iswomninnlem 15276 |
Copyright terms: Public domain | W3C validator |