This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ifptru

Description: Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue . This is essentially dedlema . (Contributed by BJ, 20-Sep-2019) (Proof shortened by Wolf Lammen, 10-Jul-2020)

Ref Expression
Assertion ifptru ⊢ φ → if- φ ψ χ ↔ ψ

Proof

Step Hyp Ref Expression
1 biimt ⊢ φ → ψ ↔ φ → ψ
2 orc ⊢ φ → φ ∨ χ
3 2 biantrud ⊢ φ → φ → ψ ↔ φ → ψ ∧ φ ∨ χ
4 dfifp3 ⊢ if- φ ψ χ ↔ φ → ψ ∧ φ ∨ χ
5 3 4 bitr4di ⊢ φ → φ → ψ ↔ if- φ ψ χ
6 1 5 bitr2d ⊢ φ → if- φ ψ χ ↔ ψ