| 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 337 | . 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃)) |
| 3 | bibi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 4 | 3 | bibi1i 338 | . 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃)) |
| 5 | 2, 4 | bitri 275 | 1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 |
| 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 207 |
| This theorem is referenced by: pm5.32 573 biadan 819 orbidi 955 pm5.7 956 xorbi12i 1524 norass 1537 rexbiOLD 3105 vn0 4345 ab0orv 4383 rexprg 4697 brsymdif 5202 nfnid 5375 asymref 6136 isocnv2 7351 zfcndrep 10654 f1omvdco3 19467 brtxpsd 35895 eliminable-abeqab 36869 bj-sbeq 36902 bj-rcleqf 37026 symrefref3 38565 eldisjn0el 38807 abbibw 42687 rp-fakeoranass 43527 rp-fakeinunass 43528 relexp0eq 43714 absnsb 47039 ichcom 47446 ichbi12i 47447 |
| Copyright terms: Public domain | W3C validator |