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