Metamath Proof Explorer

Theorem abciffcbatnabciffncba

Description: Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020)

Ref Expression
Assertion abciffcbatnabciffncba 
|- ( -. ( ( ph /\ ps ) /\ ch ) -> -. ( ( ch /\ ps ) /\ ph ) )

Proof

Step Hyp Ref Expression
1 an31 
 |-  ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) )
2 notbi 
 |-  ( ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) ) <-> ( -. ( ( ph /\ ps ) /\ ch ) <-> -. ( ( ch /\ ps ) /\ ph ) ) )
3 2 biimpi 
 |-  ( ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) ) -> ( -. ( ( ph /\ ps ) /\ ch ) <-> -. ( ( ch /\ ps ) /\ ph ) ) )
4 1 3 ax-mp 
 |-  ( -. ( ( ph /\ ps ) /\ ch ) <-> -. ( ( ch /\ ps ) /\ ph ) )
5 4 biimpi 
 |-  ( -. ( ( ph /\ ps ) /\ ch ) -> -. ( ( ch /\ ps ) /\ ph ) )