Metamath Proof Explorer


Theorem biancomd

Description: Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018)

Ref Expression
Hypothesis biancomd.1 φ ψ θ χ
Assertion biancomd φ ψ χ θ

Proof

Step Hyp Ref Expression
1 biancomd.1 φ ψ θ χ
2 ancom θ χ χ θ
3 1 2 bitrdi φ ψ χ θ