Metamath Proof Explorer


Theorem aistbistaandb

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

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

Proof

Step Hyp Ref Expression
1 aistbistaandb.1 φ
2 aistbistaandb.2 ψ
3 1 aistia φ
4 2 aistia ψ
5 3 4 pm3.2i φ ψ