Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jarvin Udandy
bisaiaisb
Next ⟩
atbiffatnnbalt
Metamath Proof Explorer
Ascii
Unicode
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
⊢
ψ
↔
φ
→
φ
↔
ψ