Metamath Proof Explorer

Theorem nanbi12

Description: Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018)

Ref Expression
Assertion nanbi12 
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph -/\ ch ) <-> ( ps -/\ th ) ) )

Proof

Step Hyp Ref Expression
1 nanbi1 
 |-  ( ( ph <-> ps ) -> ( ( ph -/\ ch ) <-> ( ps -/\ ch ) ) )
2 nanbi2 
 |-  ( ( ch <-> th ) -> ( ( ps -/\ ch ) <-> ( ps -/\ th ) ) )
3 1 2 sylan9bb 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ph -/\ ch ) <-> ( ps -/\ th ) ) )