![]() |
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 266 | . 2 ⊢ (𝜓 ↔ 𝜒) |
5 | 1, 4 | bitr3i 266 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 |
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 197 |
This theorem is referenced by: bigolden 1014 2eu8 2698 2ralor 3247 sbcco 3599 symdifass 3996 dfiin2g 4705 zfpair 5053 dffun6f 6063 fsplit 7451 axdc3lem4 9487 istrkg2ld 25579 legso 25714 disjunsn 29735 gtiso 29808 fpwrelmapffslem 29837 qqhre 30394 dfpo2 31973 dfdm5 32002 dfrn5 32003 brimg 32371 dfrecs2 32384 poimirlem25 33765 cdlemefrs29bpre0 36204 cdlemftr3 36373 dffrege115 38792 brco3f1o 38851 elnev 39159 2reu8 41716 |
Copyright terms: Public domain | W3C validator |