QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud1lem0ab Unicode version
Theorem ud1lem0ab 257
Description: Join both sides of hypotheses with ->1.
Hypotheses
Ref Expression
ud1lem0ab.1 a = b
ud1lem0ab.2 c = d
Assertion
Ref Expression
ud1lem0ab (a ->1 c) = (b ->1 d)
Proof of Theorem ud1lem0ab
StepHypRef Expression
1 ud1lem0ab.1 . . 3 a = b
21ud1lem0b 256 . 2 (a ->1 c) = (b ->1 c)
3 ud1lem0ab.2 . . 3 c = d
43ud1lem0a 255 . 2 (b ->1 c) = (b ->1 d)
52, 4ax-r2 36 1 (a ->1 c) = (b ->1 d)
Colors of variables: term
Syntax hints:   = wb 1   ->1 wi1 12
This theorem was proved from axioms:  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-i1 44
This theorem is referenced by:  1oai1  821  gomaex3  924  oa3to4lem6  950  oa4to6  965
  Copyright terms: Public domain W3C validator