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

Metamath Proof Explorer

Theorem ifnetrue

Description: Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Assertion ifnetrue ⊢ A ≠ B ∧ if φ A B = A → φ

Proof

Step Hyp Ref Expression
1 iffalse ⊢ ¬ φ → if φ A B = B
2 1 adantl ⊢ A ≠ B ∧ if φ A B = A ∧ ¬ φ → if φ A B = B
3 simplr ⊢ A ≠ B ∧ if φ A B = A ∧ ¬ φ → if φ A B = A
4 simpll ⊢ A ≠ B ∧ if φ A B = A ∧ ¬ φ → A ≠ B
5 3 4 eqnetrd ⊢ A ≠ B ∧ if φ A B = A ∧ ¬ φ → if φ A B ≠ B
6 5 neneqd ⊢ A ≠ B ∧ if φ A B = A ∧ ¬ φ → ¬ if φ A B = B
7 2 6 condan ⊢ A ≠ B ∧ if φ A B = A → φ