Description: Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | aiffbtbat.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
aiffbtbat.2 | ⊢ ( ⊤ ↔ 𝜓 ) | ||
Assertion | aiffbtbat | ⊢ ( 𝜑 ↔ ⊤ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | aiffbtbat.1 | ⊢ ( 𝜑 ↔ 𝜓 ) | |
2 | aiffbtbat.2 | ⊢ ( ⊤ ↔ 𝜓 ) | |
3 | 1 2 | bitr4i | ⊢ ( 𝜑 ↔ ⊤ ) |