Metamath Proof Explorer


Theorem anbi12ci

Description: Variant of anbi12i with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypotheses anbi12.1 φ ψ
anbi12.2 χ θ
Assertion anbi12ci φ χ θ ψ

Proof

Step Hyp Ref Expression
1 anbi12.1 φ ψ
2 anbi12.2 χ θ
3 1 2 anbi12i φ χ ψ θ
4 3 biancomi φ χ θ ψ