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 φ A A = A


Step Hyp Ref Expression
1 iftrue φ if φ A A = A
2 iffalse ¬ φ if φ A A = A
3 1 2 pm2.61i if φ A A = A