Theorem nbbnOLD

Description: Obsolete version of nbbn as of 10-Jun-2026. (Contributed by NM, 27-Jun-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nbbnOLD	|- ( ( -. ph <-> ps ) <-> -. ( ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		xor3	|- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
2		con2bi	|- ( ( ph <-> -. ps ) <-> ( ps <-> -. ph ) )
3		bicom	|- ( ( ps <-> -. ph ) <-> ( -. ph <-> ps ) )
4	1 2 3	3bitrri	|- ( ( -. ph <-> ps ) <-> -. ( ph <-> ps ) )