Metamath Proof Explorer

Theorem ifpan123g

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

Ref Expression
Assertion ifpan123g ${⊢}\left(if-\left({\phi },{\chi },{\tau }\right)\wedge if-\left({\psi },{\theta },{\eta }\right)\right)↔\left(\left(\left(¬{\phi }\vee {\chi }\right)\wedge \left({\phi }\vee {\tau }\right)\right)\wedge \left(\left(¬{\psi }\vee {\theta }\right)\wedge \left({\psi }\vee {\eta }\right)\right)\right)$

Proof

Step Hyp Ref Expression
1 dfifp4 ${⊢}if-\left({\phi },{\chi },{\tau }\right)↔\left(\left(¬{\phi }\vee {\chi }\right)\wedge \left({\phi }\vee {\tau }\right)\right)$
2 dfifp4 ${⊢}if-\left({\psi },{\theta },{\eta }\right)↔\left(\left(¬{\psi }\vee {\theta }\right)\wedge \left({\psi }\vee {\eta }\right)\right)$
3 1 2 anbi12i ${⊢}\left(if-\left({\phi },{\chi },{\tau }\right)\wedge if-\left({\psi },{\theta },{\eta }\right)\right)↔\left(\left(\left(¬{\phi }\vee {\chi }\right)\wedge \left({\phi }\vee {\tau }\right)\right)\wedge \left(\left(¬{\psi }\vee {\theta }\right)\wedge \left({\psi }\vee {\eta }\right)\right)\right)$