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 ( 𝜑𝜓 )