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
|- ( ph <-> T. )
aistbistaandb.2
|- ( ps <-> T. )
Assertion aistbistaandb
|- ( ph /\ ps )

Proof

Step Hyp Ref Expression
1 aistbistaandb.1
 |-  ( ph <-> T. )
2 aistbistaandb.2
 |-  ( ps <-> T. )
3 1 aistia
 |-  ph
4 2 aistia
 |-  ps
5 3 4 pm3.2i
 |-  ( ph /\ ps )