Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Propositions from _Begriffsschrift_
_Begriffsschrift_ Chapter II with logical equivalence
axfrege54a
Next ⟩
ax-frege54a
Metamath Proof Explorer
Ascii
Unicode
Theorem
axfrege54a
Description:
Justification for
ax-frege54a
. Identical to
biid
.
(Contributed by
RP
, 24-Dec-2019)
Ref
Expression
Assertion
axfrege54a
⊢
φ
↔
φ
Proof
Step
Hyp
Ref
Expression
1
biid
⊢
φ
↔
φ