![]() |
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 336 | . 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃)) |
3 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
4 | 3 | bibi1i 337 | . 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃)) |
5 | 2, 4 | bitri 274 | 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 572 biadan 817 orbidi 950 pm5.7 951 xorbi12i 1518 norass 1531 rexbiOLD 3095 vn0 4338 ab0OLD 4373 ab0orv 4376 rexprg 4695 brsymdif 5204 nfnid 5371 asymref 6120 isocnv2 7335 zfcndrep 10648 f1omvdco3 19443 brtxpsd 35731 eliminable-abeqab 36586 bj-sbeq 36620 bj-rcleqf 36745 symrefref3 38275 eldisjn0el 38517 abbibw 42370 rp-fakeoranass 43218 rp-fakeinunass 43219 relexp0eq 43405 absnsb 46678 ichcom 47067 ichbi12i 47068 |
Copyright terms: Public domain | W3C validator |