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

Metamath Proof Explorer

Theorem anifp

Description: The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor . (Contributed by BJ, 30-Sep-2019)

Ref Expression
Assertion anifp ⊢ ψ ∧ χ → if- φ ψ χ

Proof

Step Hyp Ref Expression
1 olc ⊢ ψ → ¬ φ ∨ ψ
2 olc ⊢ χ → φ ∨ χ
3 1 2 anim12i ⊢ ψ ∧ χ → ¬ φ ∨ ψ ∧ φ ∨ χ
4 dfifp4 ⊢ if- φ ψ χ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ
5 3 4 sylibr ⊢ ψ ∧ χ → if- φ ψ χ