Metamath Proof Explorer

Theorem ifid

Description: Identical true and false arguments in the conditional operator. (Contributed by NM, 18-Apr-2005)

Ref Expression
Assertion ifid 
|- if ( ph , A , A ) = A

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( ph -> if ( ph , A , A ) = A )
2 iffalse 
 |-  ( -. ph -> if ( ph , A , A ) = A )
3 1 2 pm2.61i 
 |-  if ( ph , A , A ) = A