This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xchnxbi

Description: Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014)

Ref Expression
Hypotheses xchnxbi.1 
|- ( -. ph <-> ps )
xchnxbi.2 
|- ( ph <-> ch )
Assertion xchnxbi 
|- ( -. ch <-> ps )

Proof

Step Hyp Ref Expression
1 xchnxbi.1 
 |-  ( -. ph <-> ps )
2 xchnxbi.2 
 |-  ( ph <-> ch )
3 2 notbii 
 |-  ( -. ph <-> -. ch )
4 3 1 bitr3i 
 |-  ( -. ch <-> ps )