Metamath Proof Explorer

Theorem ifpdfan

Description: Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020)

		Ref	Expression
	Assertion	ifpdfan	$⊢ (φ \land ψ) \leftrightarrow if- (φ, ψ, ⊥)$

Step	Hyp	Ref	Expression
1		fal	$⊢ \neg ⊥$
2	1	intnan	$⊢ \neg (\neg φ \land ⊥)$
3	2	biorfri	$⊢ (φ \land ψ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land ⊥))$
4		df-ifp	$⊢ if- (φ, ψ, ⊥) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land ⊥))$
5	3 4	bitr4i	$⊢ (φ \land ψ) \leftrightarrow if- (φ, ψ, ⊥)$