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- ψ θ η ¬ φ χ φ τ ¬ ψ θ ψ η