Metamath Proof Explorer


Theorem nanbi2i

Description: Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 nanbii.1
 |-  ( ph <-> ps )
2 nanbi2
 |-  ( ( ph <-> ps ) -> ( ( ch -/\ ph ) <-> ( ch -/\ ps ) ) )
3 1 2 ax-mp
 |-  ( ( ch -/\ ph ) <-> ( ch -/\ ps ) )