Theorem ifpimimb 44463

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 1080	. 2 ⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ ((𝜑 → (𝜓 → 𝜒)) ∧ (¬ 𝜑 → (𝜃 → 𝜏))))
2		imor 867	. . . 4 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (¬ 𝜑 ∨ (𝜓 → 𝜒)))
3		pm4.8 398	. . . . . 6 ⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑)
4	3	bicomi 227	. . . . 5 ⊢ (¬ 𝜑 ↔ (𝜑 → ¬ 𝜑))
5	4	orbi1i 927	. . . 4 ⊢ ((¬ 𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)))
6		id 23	. . . . . 6 ⊢ (𝜑 → 𝜑)
7	6	orci 879	. . . . 5 ⊢ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))
8	7	biantru 539	. . . 4 ⊢ (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ↔ (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))))
9	2, 5, 8	3bitri 300	. . 3 ⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))))
10		pm4.64 863	. . . 4 ⊢ ((¬ 𝜑 → (𝜃 → 𝜏)) ↔ (𝜑 ∨ (𝜃 → 𝜏)))
11		pm4.81 399	. . . . . 6 ⊢ ((¬ 𝜑 → 𝜑) ↔ 𝜑)
12	11	bicomi 227	. . . . 5 ⊢ (𝜑 ↔ (¬ 𝜑 → 𝜑))
13	12	orbi1i 927	. . . 4 ⊢ ((𝜑 ∨ (𝜃 → 𝜏)) ↔ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))
14	6	orci 879	. . . . 5 ⊢ ((𝜑 → 𝜑) ∨ (𝜓 → 𝜏))
15	14	biantrur 540	. . . 4 ⊢ (((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)) ↔ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))))
16	10, 13, 15	3bitri 300	. . 3 ⊢ ((¬ 𝜑 → (𝜃 → 𝜏)) ↔ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏))))
17	9, 16	anbi12i 640	. 2 ⊢ (((𝜑 → (𝜓 → 𝜒)) ∧ (¬ 𝜑 → (𝜃 → 𝜏))) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))))
18		ifpim123g 44459	. . 3 ⊢ ((if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)) ↔ ((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))))
19	18	bicomi 227	. 2 ⊢ (((((𝜑 → ¬ 𝜑) ∨ (𝜓 → 𝜒)) ∧ ((𝜑 → 𝜑) ∨ (𝜃 → 𝜒))) ∧ (((𝜑 → 𝜑) ∨ (𝜓 → 𝜏)) ∧ ((¬ 𝜑 → 𝜑) ∨ (𝜃 → 𝜏)))) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))
20	1, 17, 19	3bitri 300	1 ⊢ (if-(𝜑, (𝜓 → 𝜒), (𝜃 → 𝜏)) ↔ (if-(𝜑, 𝜓, 𝜃) → if-(𝜑, 𝜒, 𝜏)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  if-wif 1078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079

This theorem is used by:  ifpororb  44464  ifpbibib  44469