Metamath Proof Explorer


Theorem aistia

Description: Given a is equivalent to T. , there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016)

Ref Expression
Hypothesis aistia.1
|- ( ph <-> T. )
Assertion aistia
|- ph

Proof

Step Hyp Ref Expression
1 aistia.1
 |-  ( ph <-> T. )
2 tbtru
 |-  ( ph <-> ( ph <-> T. ) )
3 1 2 mpbir
 |-  ph