Theorem ifpimimb 41324

Description: Factor conditional logic operator over implication in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)

Assertion

Ref	Expression
ifpimimb	⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))

Proof of Theorem ifpimimb

Step	Hyp	Ref	Expression
1		dfifp2 1063	. 2 ⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ ((𝜑 → (𝜓 → 𝜒)) ∧ (¬ 𝜑 → (𝜃 → 𝜏))))
2		imor 851	. . . 4 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (¬ 𝜑 ∨ (𝜓 → 𝜒)))
3		pm4.8 394	. . . . . 6 ⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑)
4	3	bicomi 223	. . . . 5 ⊢ (¬ 𝜑 ↔ (𝜑 → ¬ 𝜑))
5	4	orbi1i 912	. . . 4 ⊢ ((¬ 𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)))
6		id 22	. . . . . 6 ⊢ (𝜑 → 𝜑)
7	6	orci 863	. . . . 5 ⊢ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))
8	7	biantru 531	. . . 4 ⊢ (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ↔ (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))))
9	2, 5, 8	3bitri 297	. . 3 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))))
10		pm4.64 847	. . . 4 ⊢ ((¬ 𝜑 → (𝜃 → 𝜏)) ↔ (𝜑 ∨ (𝜃 → 𝜏)))
11		pm4.81 395	. . . . . 6 ⊢ ((¬ 𝜑 → 𝜑) ↔ 𝜑)
12	11	bicomi 223	. . . . 5 ⊢ (𝜑 ↔ (¬ 𝜑 → 𝜑))
13	12	orbi1i 912	. . . 4 ⊢ ((𝜑 ∨ (𝜃 → 𝜏)) ↔ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))
14	6	orci 863	. . . . 5 ⊢ ((𝜑 → 𝜑) ∨ (𝜓 → 𝜏))
15	14	biantrur 532	. . . 4 ⊢ (((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)) ↔ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))))
16	10, 13, 15	3bitri 297	. . 3 ⊢ ((¬ 𝜑 → (𝜃 → 𝜏)) ↔ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))))
17	9, 16	anbi12i 628	. 2 ⊢ (((𝜑 → (𝜓 → 𝜒)) ∧ (¬ 𝜑 → (𝜃 → 𝜏))) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))))
18		ifpim123g 41320	. . 3 ⊢ ((if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))))
19	18	bicomi 223	. 2 ⊢ (((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
20	1, 17, 19	3bitri 297	1 ⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 845  if-wif 1061

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  df-an 398  df-or 846  df-ifp 1062

This theorem is referenced by:  ifpororb  41325  ifpbibib  41330