Metamath Proof Explorer

Theorem dfifp7

Description: Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019)

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

Proof

Step Hyp Ref Expression
1 orcom ⊢ φ ∧ ψ ∨ ¬ χ → φ ↔ ¬ χ → φ ∨ φ ∧ ψ
2 dfifp6 ⊢ if- φ ψ χ ↔ φ ∧ ψ ∨ ¬ χ → φ
3 imor ⊢ χ → φ → φ ∧ ψ ↔ ¬ χ → φ ∨ φ ∧ ψ
4 1 2 3 3bitr4i ⊢ if- φ ψ χ ↔ χ → φ → φ ∧ ψ