Metamath Proof Explorer


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 ψ φ φ ψ