Metamath Proof Explorer


Theorem iftrue

Description: Value of the conditional operator when its first argument is true. (Contributed by NM, 15-May-1999) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion iftrue φ if φ A B = A

Proof

Step Hyp Ref Expression
1 dfif2 if φ A B = x | x B φ x A φ
2 dedlem0a φ x A x B φ x A φ
3 2 abbi2dv φ A = x | x B φ x A φ
4 1 3 eqtr4id φ if φ A B = A