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- φ ψ χ ↔ φ ∧ ψ → χ ∧ φ ∧ χ → ψ