Metamath Proof Explorer


Theorem ifpid3g

Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpid3g χ if- φ ψ χ φ ψ χ φ χ ψ

Proof

Step Hyp Ref Expression
1 olc χ φ χ
2 1 1 pm3.2i χ φ χ χ φ χ
3 ifpidg χ if- φ ψ χ φ ψ χ φ χ ψ χ φ χ χ φ χ
4 2 3 mpbiran2 χ if- φ ψ χ φ ψ χ φ χ ψ