Metamath Proof Explorer


Theorem aisbbisfaisf

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

Ref Expression
Hypotheses aisbbisfaisf.1 ⊢ ( 𝜑 ↔ 𝜓 )
aisbbisfaisf.2 ⊢ ( 𝜓 ↔ ⊥ )
Assertion aisbbisfaisf ( 𝜑 ↔ ⊥ )

Proof

Step Hyp Ref Expression
1 aisbbisfaisf.1 ⊢ ( 𝜑 ↔ 𝜓 )
2 aisbbisfaisf.2 ⊢ ( 𝜓 ↔ ⊥ )
3 1 2 bitri ⊢ ( 𝜑 ↔ ⊥ )