Metamath Proof Explorer

Theorem cadtru

Description: The adder carry is true as soon as its first two inputs are the truth constant. (Contributed by Mario Carneiro, 4-Sep-2016)

		Ref	Expression
	Assertion	cadtru	$⊢ cadd (⊤, ⊤, φ)$

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2		cad11	$⊢ (⊤ \land ⊤) \to cadd (⊤, ⊤, φ)$
3	1 1 2	mp2an	$⊢ cadd (⊤, ⊤, φ)$