Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Giovanni Mascellani
Tools for automatic proof building
tradd
Next ⟩
gm-sbtru
Metamath Proof Explorer
Ascii
Unicode
Theorem
tradd
Description:
Add top ad a conjunct.
(Contributed by
Giovanni Mascellani
, 24-May-2019)
Ref
Expression
Hypothesis
tradd.1
⊢
φ
↔
ψ
Assertion
tradd
⊢
φ
↔
⊤
∧
ψ
Proof
Step
Hyp
Ref
Expression
1
tradd.1
⊢
φ
↔
ψ
2
truan
⊢
⊤
∧
ψ
↔
ψ
3
1
2
bitr4i
⊢
φ
↔
⊤
∧
ψ