![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bibi12i | Structured version Visualization version GIF version |
Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
bibi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
bibi12i.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
bibi12i | ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bibi12i.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
2 | 1 | bibi2i 338 | . 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃)) |
3 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | bibi1i 339 | . 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃)) |
5 | 2, 4 | bitri 275 | 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: pm5.32 575 biadan 818 orbidi 952 pm5.7 953 xorbi12i 1524 xorbi12iOLD 1525 norass 1539 rexbiOLD 3109 vn0 4299 ab0OLD 4336 ab0orv 4339 rexprg 4658 brsymdif 5165 nfnid 5331 asymref 6071 isocnv2 7277 zfcndrep 10551 f1omvdco3 19232 brtxpsd 34482 eliminable-abeqab 35337 bj-sbeq 35371 bj-rcleqf 35499 symrefref3 37029 eldisjn0el 37271 rp-fakeoranass 41793 rp-fakeinunass 41794 relexp0eq 41980 absnsb 45268 ichcom 45658 ichbi12i 45659 |
Copyright terms: Public domain | W3C validator |