Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  or4 GIF version

Theorem or4 84
 Description: Swap disjuncts.
Assertion
Ref Expression
or4 ((ab) ∪ (cd)) = ((ac) ∪ (bd))

Proof of Theorem or4
StepHypRef Expression
1 or12 80 . . 3 (b ∪ (cd)) = (c ∪ (bd))
21lor 70 . 2 (a ∪ (b ∪ (cd))) = (a ∪ (c ∪ (bd)))
3 ax-a3 32 . 2 ((ab) ∪ (cd)) = (a ∪ (b ∪ (cd)))
4 ax-a3 32 . 2 ((ac) ∪ (bd)) = (a ∪ (c ∪ (bd)))
52, 3, 43tr1 63 1 ((ab) ∪ (cd)) = ((ac) ∪ (bd))
 Colors of variables: term Syntax hints:   = wb 1   ∪ wo 6 This theorem was proved from axioms:  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38 This theorem is referenced by:  or42  85  orordi  112  orordir  113  cmtrcom  190  womle2a  295  k1-2  357  k1-3  358  wcom2or  427  com2or  483  i3con  551  ud1lem3  562  ud4lem1c  579  ud4lem1  581  ud4lem3b  584  ud5lem3  594  u4lem5  764  3vth6  809  3vded22  818  wdwom  1104  dp41lemf  1186  dp41leml  1191  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
 Copyright terms: Public domain W3C validator