Metamath Proof Explorer


Theorem aiffbbtat

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

Ref Expression
Hypotheses aiffbbtat.1
|- ( ph <-> ps )
aiffbbtat.2
|- ( ps <-> T. )
Assertion aiffbbtat
|- ( ph <-> T. )

Proof

Step Hyp Ref Expression
1 aiffbbtat.1
 |-  ( ph <-> ps )
2 aiffbbtat.2
 |-  ( ps <-> T. )
3 1 2 bitri
 |-  ( ph <-> T. )