Theorem ifpan23

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

	Ref	Expression
Assertion	ifpan23	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜒 ) ∧ if- ( 𝜑 , 𝜃 , 𝜏 ) ) ↔ if- ( 𝜑 , ( 𝜓 ∧ 𝜃 ) , ( 𝜒 ∧ 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ifpan123g	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜒 ) ∧ if- ( 𝜑 , 𝜃 , 𝜏 ) ) ↔ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( ( ¬ 𝜑 ∨ 𝜃 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ) )
2		an4	⊢ ( ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( 𝜑 ∨ 𝜒 ) ) ∧ ( ( ¬ 𝜑 ∨ 𝜃 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ) ↔ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜃 ) ) ∧ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ) )
3		dfifp4	⊢ ( if- ( 𝜑 , ( 𝜓 ∧ 𝜃 ) , ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( ¬ 𝜑 ∨ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜑 ∨ ( 𝜒 ∧ 𝜏 ) ) ) )
4		ordi	⊢ ( ( ¬ 𝜑 ∨ ( 𝜓 ∧ 𝜃 ) ) ↔ ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜃 ) ) )
5		ordi	⊢ ( ( 𝜑 ∨ ( 𝜒 ∧ 𝜏 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
6	4 5	anbi12i	⊢ ( ( ( ¬ 𝜑 ∨ ( 𝜓 ∧ 𝜃 ) ) ∧ ( 𝜑 ∨ ( 𝜒 ∧ 𝜏 ) ) ) ↔ ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜃 ) ) ∧ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ) )
7	3 6	bitr2i	⊢ ( ( ( ( ¬ 𝜑 ∨ 𝜓 ) ∧ ( ¬ 𝜑 ∨ 𝜃 ) ) ∧ ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ) ↔ if- ( 𝜑 , ( 𝜓 ∧ 𝜃 ) , ( 𝜒 ∧ 𝜏 ) ) )
8	1 2 7	3bitri	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜒 ) ∧ if- ( 𝜑 , 𝜃 , 𝜏 ) ) ↔ if- ( 𝜑 , ( 𝜓 ∧ 𝜃 ) , ( 𝜒 ∧ 𝜏 ) ) )