Theorem biadanOLD 854

Description: Obsolete version of biadan 853 as of 8-Mar-2023. (Contributed by BJ, 4-Mar-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
biadanOLD	⊢ ((𝜑 → 𝜓) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))

Proof of Theorem biadanOLD

Step	Hyp	Ref	Expression
1		pm5.32 569	. . . . . 6 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ ((𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒)))
2		bicom 214	. . . . . 6 ⊢ (((𝜓 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑)))
3	1, 2	bitri 267	. . . . 5 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑)))
4		biass 376	. . . . 5 ⊢ ((((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ 𝜑)) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑))))
5	3, 4	mpbir 223	. . . 4 ⊢ (((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ 𝜑))
6		pm4.71r 554	. . . . 5 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑)))
7		biass 376	. . . . 5 ⊢ ((((𝜑 → 𝜓) ↔ 𝜑) ↔ (𝜓 ∧ 𝜑)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑))))
8	6, 7	mpbir 223	. . . 4 ⊢ (((𝜑 → 𝜓) ↔ 𝜑) ↔ (𝜓 ∧ 𝜑))
9	5, 8	bitr4i 270	. . 3 ⊢ (((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ 𝜑))
10		bicom 214	. . . 4 ⊢ ((((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ 𝜑)) ↔ (((𝜑 → 𝜓) ↔ 𝜑) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒))))
11		biass 376	. . . 4 ⊢ ((((𝜑 → 𝜓) ↔ 𝜑) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒))) ↔ ((𝜑 → 𝜓) ↔ (𝜑 ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)))))
12		bicom 214	. . . . . . 7 ⊢ (((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 → (𝜑 ↔ 𝜒))))
13	12	bibi2i 329	. . . . . 6 ⊢ ((𝜑 ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒))) ↔ (𝜑 ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 → (𝜑 ↔ 𝜒)))))
14		biass 376	. . . . . 6 ⊢ (((𝜑 ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 → (𝜑 ↔ 𝜒))) ↔ (𝜑 ↔ ((𝜓 ∧ 𝜒) ↔ (𝜓 → (𝜑 ↔ 𝜒)))))
15	13, 14	bitr4i 270	. . . . 5 ⊢ ((𝜑 ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒))) ↔ ((𝜑 ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 → (𝜑 ↔ 𝜒))))
16	15	bibi2i 329	. . . 4 ⊢ (((𝜑 → 𝜓) ↔ (𝜑 ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)))) ↔ ((𝜑 → 𝜓) ↔ ((𝜑 ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 → (𝜑 ↔ 𝜒)))))
17	10, 11, 16	3bitri 289	. . 3 ⊢ ((((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ 𝜑)) ↔ ((𝜑 → 𝜓) ↔ ((𝜑 ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 → (𝜑 ↔ 𝜒)))))
18	9, 17	mpbi 222	. 2 ⊢ ((𝜑 → 𝜓) ↔ ((𝜑 ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 → (𝜑 ↔ 𝜒))))
19		bicom 214	. 2 ⊢ (((𝜑 ↔ (𝜓 ∧ 𝜒)) ↔ (𝜓 → (𝜑 ↔ 𝜒))) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))
20	18, 19	bitri 267	1 ⊢ ((𝜑 → 𝜓) ↔ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by: (None)