Metamath Proof Explorer


Theorem ifpdfan2

Description: Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpdfan2 φ ψ if- φ ψ φ

Proof

Step Hyp Ref Expression
1 id φ φ
2 1 notnoti ¬ ¬ φ φ
3 2 biorfi φ ψ φ ψ ¬ φ φ
4 dfifp6 if- φ ψ φ φ ψ ¬ φ φ
5 3 4 bitr4i φ ψ if- φ ψ φ