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 ( 𝜑𝜓 )
Assertion nanbi2i ( ( 𝜒𝜑 ) ↔ ( 𝜒𝜓 ) )

Proof

Step Hyp Ref Expression
1 nanbii.1 ( 𝜑𝜓 )
2 nanbi2 ( ( 𝜑𝜓 ) → ( ( 𝜒𝜑 ) ↔ ( 𝜒𝜓 ) ) )
3 1 2 ax-mp ( ( 𝜒𝜑 ) ↔ ( 𝜒𝜓 ) )