Metamath Proof Explorer


Theorem astbstanbst

Description: Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016)

Ref Expression
Hypotheses astbstanbst.1 φ
astbstanbst.2 ψ
Assertion astbstanbst φ ψ

Proof

Step Hyp Ref Expression
1 astbstanbst.1 φ
2 astbstanbst.2 ψ
3 1 aistia φ
4 2 aistia ψ
5 3 4 pm3.2i φ ψ
6 5 bitru φ ψ