Theorem ifpor123g

Description: Disjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020)

	Ref	Expression
Assertion	ifpor123g	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) ∨ if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-or	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) ∨ if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) )
2		ifpnot23	⊢ ( ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) ↔ if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) )
3	2	imbi1i	⊢ ( ( ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) )
4	1 3	bitri	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) ∨ if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) )
5		ifpim123g	⊢ ( ( if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) → if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜂 ) ) ) ) )
6	4 5	bitri	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) ∨ if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜂 ) ) ) ) )
7		pm4.64	⊢ ( ( ¬ 𝜒 → 𝜃 ) ↔ ( 𝜒 ∨ 𝜃 ) )
8	7	orbi2i	⊢ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 → 𝜃 ) ) ↔ ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) )
9		pm4.64	⊢ ( ( ¬ 𝜏 → 𝜃 ) ↔ ( 𝜏 ∨ 𝜃 ) )
10	9	orbi2i	⊢ ( ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜃 ) ) ↔ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜃 ) ) )
11	8 10	anbi12i	⊢ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜃 ) ) ) ↔ ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜃 ) ) ) )
12		pm4.64	⊢ ( ( ¬ 𝜒 → 𝜂 ) ↔ ( 𝜒 ∨ 𝜂 ) )
13	12	orbi2i	⊢ ( ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 → 𝜂 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ 𝜂 ) ) )
14		pm4.64	⊢ ( ( ¬ 𝜏 → 𝜂 ) ↔ ( 𝜏 ∨ 𝜂 ) )
15	14	orbi2i	⊢ ( ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜂 ) ) ↔ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜂 ) ) )
16	13 15	anbi12i	⊢ ( ( ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜂 ) ) ) ↔ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ) )
17	11 16	anbi12i	⊢ ( ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( ¬ 𝜒 → 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( ¬ 𝜒 → 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( ¬ 𝜏 → 𝜂 ) ) ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ) ) )
18	6 17	bitri	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) ∨ if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ( 𝜑 → ¬ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∧ ( ( 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜃 ) ) ) ∧ ( ( ( 𝜑 → 𝜓 ) ∨ ( 𝜒 ∨ 𝜂 ) ) ∧ ( ( ¬ 𝜓 → 𝜑 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ) ) )