Metamath Proof Explorer

Theorem anbi1ci

Description: Variant of anbi1i with commutation. (Contributed by Peter Mazsa, 7-Mar-2020)

Ref Expression
Hypothesis anbi.1 
|- ( ph <-> ps )
Assertion anbi1ci 
|- ( ( ch /\ ph ) <-> ( ps /\ ch ) )

Proof

Step Hyp Ref Expression
1 anbi.1 
 |-  ( ph <-> ps )
2 1 anbi2i 
 |-  ( ( ch /\ ph ) <-> ( ch /\ ps ) )
3 2 biancomi 
 |-  ( ( ch /\ ph ) <-> ( ps /\ ch ) )