Theorem ifpdfnan

Description: Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020)

	Ref	Expression
Assertion	ifpdfnan	|- ( ( ph -/\ ps ) <-> if- ( ph , -. ps , T. ) )

Proof

Step	Hyp	Ref	Expression
1		df-nan	|- ( ( ph -/\ ps ) <-> -. ( ph /\ ps ) )
2		ifpdfan	|- ( ( ph /\ ps ) <-> if- ( ph , ps , F. ) )
3	2	notbii	|- ( -. ( ph /\ ps ) <-> -. if- ( ph , ps , F. ) )
4		ifpnot23	|- ( -. if- ( ph , ps , F. ) <-> if- ( ph , -. ps , -. F. ) )
5		notfal	|- ( -. F. <-> T. )
6		ifpbi3	|- ( ( -. F. <-> T. ) -> ( if- ( ph , -. ps , -. F. ) <-> if- ( ph , -. ps , T. ) ) )
7	5 6	ax-mp	|- ( if- ( ph , -. ps , -. F. ) <-> if- ( ph , -. ps , T. ) )
8	4 7	bitri	|- ( -. if- ( ph , ps , F. ) <-> if- ( ph , -. ps , T. ) )
9	1 3 8	3bitri	|- ( ( ph -/\ ps ) <-> if- ( ph , -. ps , T. ) )