![]() |
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 277 | . 2 ⊢ (𝜓 ↔ 𝜒) |
5 | 1, 4 | bitr3i 277 | 1 ⊢ (𝜃 ↔ 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 |
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 206 |
This theorem is referenced by: bigolden 1026 sb8f 2350 2eu8 2659 2ralorOLD 3221 sbccow 3763 sbcco 3766 dfiin2g 4993 zfpair 5377 dfpo2 6249 dffun6f 6515 fnssintima 7308 imaeqsexv 7309 fsplit 8050 axdc3lem4 10390 addsunif 27313 addsasslem1 27314 addsasslem2 27315 istrkg2ld 27405 legso 27544 disjunsn 31515 gtiso 31617 fpwrelmapffslem 31652 qqhre 32604 satfdm 33966 dfdm5 34350 dfrn5 34351 brimg 34525 dfrecs2 34538 poimirlem25 36106 cdlemefrs29bpre0 38862 cdlemftr3 39031 dffrege115 42257 brco3f1o 42312 elnev 42725 2reu8 45351 ichbi12i 45659 i0oii 46959 |
Copyright terms: Public domain | W3C validator |