Metamath Proof Explorer


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 φ ψ