Metamath Proof Explorer


Theorem nanbi1i

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

Ref Expression
Hypothesis nanbii.1 ( 𝜑𝜓 )
Assertion nanbi1i ( ( 𝜑𝜒 ) ↔ ( 𝜓𝜒 ) )

Proof

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