Theorem ifpan123g

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

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

Proof

Step	Hyp	Ref	Expression
1		dfifp4	⊢ ( if- ( 𝜑 , 𝜒 , 𝜏 ) ↔ ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) )
2		dfifp4	⊢ ( if- ( 𝜓 , 𝜃 , 𝜂 ) ↔ ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) )
3	1 2	anbi12i	⊢ ( ( if- ( 𝜑 , 𝜒 , 𝜏 ) ∧ if- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ¬ 𝜑 ∨ 𝜒 ) ∧ ( 𝜑 ∨ 𝜏 ) ) ∧ ( ( ¬ 𝜓 ∨ 𝜃 ) ∧ ( 𝜓 ∨ 𝜂 ) ) ) )