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 265 | . 2 ⊢ (𝜓 ↔ 𝜒) |
5 | 1, 4 | bitr3i 265 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 |
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 196 |
This theorem is referenced by: bigolden 972 2eu8 2548 2ralor 3088 sbcco 3425 symdifass 3815 dfiin2g 4489 zfpair 4831 dffun6f 5818 fsplit 7169 axdc3lem4 9158 istrkg2ld 25159 legso 25294 disjunsn 28789 gtiso 28861 fpwrelmapffslem 28895 qqhre 29392 dfpo2 30898 dfdm5 30921 dfrn5 30922 nofulllem5 31105 brimg 31214 dfrecs2 31227 poimirlem25 32604 cdlemefrs29bpre0 34702 cdlemftr3 34871 dffrege115 37292 brco3f1o 37351 elnev 37661 2reu8 39841 |
Copyright terms: Public domain | W3C validator |