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 ( ⊤ , ⊤ , 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		tru	⊢ ⊤
2		cad11	⊢ ( ( ⊤ ∧ ⊤ ) → cadd ( ⊤ , ⊤ , 𝜑 ) )
3	1 1 2	mp2an	⊢ cadd ( ⊤ , ⊤ , 𝜑 )