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 ( T. , T. , ph )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 cad11 
 |-  ( ( T. /\ T. ) -> cadd ( T. , T. , ph ) )
3 1 1 2 mp2an 
 |-  cadd ( T. , T. , ph )