Theorem had0OLD

Description: Obsolete version of had0 as of 10-Aug-2026. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jul-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	had0OLD	|- ( -. ph -> ( hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		had1OLD	|- ( -. ph -> ( hadd ( -. ph , -. ps , -. ch ) <-> ( -. ps <-> -. ch ) ) )
2		hadnot	|- ( -. hadd ( ph , ps , ch ) <-> hadd ( -. ph , -. ps , -. ch ) )
3		xnor	|- ( ( ps <-> ch ) <-> -. ( ps \/_ ch ) )
4		notbi	|- ( ( ps <-> ch ) <-> ( -. ps <-> -. ch ) )
5	3 4	bitr3i	|- ( -. ( ps \/_ ch ) <-> ( -. ps <-> -. ch ) )
6	1 2 5	3bitr4g	|- ( -. ph -> ( -. hadd ( ph , ps , ch ) <-> -. ( ps \/_ ch ) ) )
7	6	con4bid	|- ( -. ph -> ( hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )