Theorem bisaiaisb

Description: Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016)

	Ref	Expression
Assertion	bisaiaisb	⊢ ( ( 𝜓 ↔ 𝜑 ) → ( 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bicom1	⊢ ( ( 𝜓 ↔ 𝜑 ) → ( 𝜑 ↔ 𝜓 ) )