Description: A -/\ identity. (Contributed by Anthony Hart, 23-Oct-2010) (Proof shortened by Andrew Salmon, 13-May-2011) (Proof shortened by Wolf Lammen, 10-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | trunanfal | |- ( ( T. -/\ F. ) <-> T. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nan | |- ( ( T. -/\ F. ) <-> -. ( T. /\ F. ) ) |
|
| 2 | truanfal | |- ( ( T. /\ F. ) <-> F. ) |
|
| 3 | 1 2 | xchbinx | |- ( ( T. -/\ F. ) <-> -. F. ) |
| 4 | notfal | |- ( -. F. <-> T. ) |
|
| 5 | 3 4 | bitri | |- ( ( T. -/\ F. ) <-> T. ) |