Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Truth tables
Conjunction
falanfal
Next ⟩
Disjunction
Metamath Proof Explorer
Unicode
Structured
Theorem
falanfal
Description:
A
/\
identity.
(Contributed by
Anthony Hart
, 22-Oct-2010)
Ref
Expression
Assertion
falanfal
|- ( ( F. /\ F. ) <-> F. )
Proof
Step
Hyp
Ref
Expression
1
anidm
|- ( ( F. /\ F. ) <-> F. )