Metamath Proof Explorer

Theorem ifpid2g

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

Ref Expression
Assertion ifpid2g ⊢ ψ ↔ if- φ ψ χ ↔ ψ → φ ∨ χ ∧ χ → φ ∨ ψ

Proof

Step Hyp Ref Expression
1 ifpidg ⊢ ψ ↔ if- φ ψ χ ↔ φ ∧ ψ → ψ ∧ φ ∧ ψ → ψ ∧ χ → φ ∨ ψ ∧ ψ → φ ∨ χ
2 simpr ⊢ φ ∧ ψ → ψ
3 2 2 pm3.2i ⊢ φ ∧ ψ → ψ ∧ φ ∧ ψ → ψ
4 3 biantrur ⊢ χ → φ ∨ ψ ∧ ψ → φ ∨ χ ↔ φ ∧ ψ → ψ ∧ φ ∧ ψ → ψ ∧ χ → φ ∨ ψ ∧ ψ → φ ∨ χ
5 ancom ⊢ χ → φ ∨ ψ ∧ ψ → φ ∨ χ ↔ ψ → φ ∨ χ ∧ χ → φ ∨ ψ
6 1 4 5 3bitr2i ⊢ ψ ↔ if- φ ψ χ ↔ ψ → φ ∨ χ ∧ χ → φ ∨ ψ