bibi1i - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bibi1i		Structured version Visualization version GIF version

Theorem bibi1i 337

Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)

**Hypothesis**
Ref	Expression
bibi2i.1	⊢ (𝜑 ↔ 𝜓)

**Assertion**
Ref	Expression
bibi1i	⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))

**Proof of Theorem bibi1i**
Step	Hyp	Ref	Expression
1		bicom 221	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	bibi2i 336	. 2 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
4		bicom 221	. 2 ⊢ ((𝜒 ↔ 𝜓) ↔ (𝜓 ↔ 𝜒))
5	1, 3, 4	3bitri 296	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: bibi12i 338 biluk 384 biadaniALT 819 nanass 1504 xorass 1509 hadbi 1592 hadcoma 1593 hadnot 1596 sbrbis 2300 csbied 3930 dfss2 3965 ssequn1 4181 ab0w 4378 asymref 6128 aceq1 10160 aceq0 10161 zfac 10503 zfcndac 10662 hashreprin 34466 axacprim 35529 eliminable-abeqv 36572 wl-3xorcoma 37185 wl-3xornot 37188 redundpbi1 38329 onsupmaxb 42904 rp-fakeanorass 43180 ichn 47028 dfich2 47030

	
		OSZAR »