Theorem ifpororb

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

	Ref	Expression
Assertion	ifpororb	⊢ ( if- ( 𝜑 , ( 𝜓 ∨ 𝜒 ) , ( 𝜃 ∨ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfifp2	⊢ ( if- ( 𝜑 , ( 𝜓 ∨ 𝜒 ) , ( 𝜃 ∨ 𝜏 ) ) ↔ ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ) )
2		df-or	⊢ ( ( 𝜓 ∨ 𝜒 ) ↔ ( ¬ 𝜓 → 𝜒 ) )
3	2	imbi2i	⊢ ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ↔ ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) )
4		df-or	⊢ ( ( 𝜃 ∨ 𝜏 ) ↔ ( ¬ 𝜃 → 𝜏 ) )
5	4	imbi2i	⊢ ( ( ¬ 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ↔ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) )
6	3 5	anbi12i	⊢ ( ( ( 𝜑 → ( 𝜓 ∨ 𝜒 ) ) ∧ ( ¬ 𝜑 → ( 𝜃 ∨ 𝜏 ) ) ) ↔ ( ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) )
7		ifpimimb	⊢ ( if- ( 𝜑 , ( ¬ 𝜓 → 𝜒 ) , ( ¬ 𝜃 → 𝜏 ) ) ↔ ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
8		dfifp2	⊢ ( if- ( 𝜑 , ( ¬ 𝜓 → 𝜒 ) , ( ¬ 𝜃 → 𝜏 ) ) ↔ ( ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) )
9		imor	⊢ ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
10		ifpnot23d	⊢ ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ↔ if- ( 𝜑 , 𝜓 , 𝜃 ) )
11	10	orbi1i	⊢ ( ( ¬ if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
12	9 11	bitri	⊢ ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) → if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
13	7 8 12	3bitr3i	⊢ ( ( ( 𝜑 → ( ¬ 𝜓 → 𝜒 ) ) ∧ ( ¬ 𝜑 → ( ¬ 𝜃 → 𝜏 ) ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
14	1 6 13	3bitri	⊢ ( if- ( 𝜑 , ( 𝜓 ∨ 𝜒 ) , ( 𝜃 ∨ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )