Metamath Proof Explorer


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- ( 𝜓 , 𝜃 , 𝜂 ) ) ↔ ( ( ( ¬ 𝜑𝜒 ) ∧ ( 𝜑𝜏 ) ) ∧ ( ( ¬ 𝜓𝜃 ) ∧ ( 𝜓𝜂 ) ) ) )