Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3bitr3ri | Structured version Visualization version GIF version |
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
3bitr3i.1 | ⊢ (𝜑 ↔ 𝜓) |
3bitr3i.2 | ⊢ (𝜑 ↔ 𝜒) |
3bitr3i.3 | ⊢ (𝜓 ↔ 𝜃) |
Ref | Expression |
---|---|
3bitr3ri | ⊢ (𝜃 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr3i.3 | . 2 ⊢ (𝜓 ↔ 𝜃) | |
2 | 3bitr3i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 3bitr3i.2 | . . 3 ⊢ (𝜑 ↔ 𝜒) | |
4 | 2, 3 | bitr3i 280 | . 2 ⊢ (𝜓 ↔ 𝜒) |
5 | 1, 4 | bitr3i 280 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 |
This theorem is referenced by: bigolden 1027 2eu8 2659 2ralor 3278 sbccow 3714 sbcco 3717 dfiin2g 4938 zfpair 5311 dffun6f 6391 fsplit 7882 fsplitOLD 7883 axdc3lem4 10064 istrkg2ld 26548 legso 26687 disjunsn 30649 gtiso 30750 fpwrelmapffslem 30784 qqhre 31679 satfdm 33041 fnssintima 33388 imaeqsexv 33403 dfpo2 33438 dfdm5 33463 dfrn5 33464 brimg 33973 dfrecs2 33986 poimirlem25 35537 cdlemefrs29bpre0 38145 cdlemftr3 38314 dffrege115 41261 brco3f1o 41318 elnev 41727 2reu8 44274 ichbi12i 44583 i0oii 45884 |
Copyright terms: Public domain | W3C validator |