Description: A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010) (Proof shortened by Andrew Salmon, 13-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | falorfal | |- ( ( F. \/ F. ) <-> F. ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oridm | |- ( ( F. \/ F. ) <-> F. ) |