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

Axiom ax-arg 1153
 Description: The Arguesian law as an axiom. (Contributed by NM, 1-Apr-2012.)
Hypothesis
Ref Expression
arg.1 ((a0b0) ∩ (a1b1)) ≤ (a2b2)
Assertion
Ref Expression
ax-arg ((a0a1) ∩ (b0b1)) ≤ (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))

Detailed syntax breakdown of Axiom ax-arg
StepHypRef Expression
1 wva0 . . . 4 term  a0
2 wva1 . . . 4 term  a1
31, 2wo 6 . . 3 term  (a0a1)
4 wvb0 . . . 4 term  b0
5 wvb1 . . . 4 term  b1
64, 5wo 6 . . 3 term  (b0b1)
73, 6wa 7 . 2 term  ((a0a1) ∩ (b0b1))
8 wva2 . . . . 5 term  a2
91, 8wo 6 . . . 4 term  (a0a2)
10 wvb2 . . . . 5 term  b2
114, 10wo 6 . . . 4 term  (b0b2)
129, 11wa 7 . . 3 term  ((a0a2) ∩ (b0b2))
132, 8wo 6 . . . 4 term  (a1a2)
145, 10wo 6 . . . 4 term  (b1b2)
1513, 14wa 7 . . 3 term  ((a1a2) ∩ (b1b2))
1612, 15wo 6 . 2 term  (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))
177, 16wle 2 1 wff  ((a0a1) ∩ (b0b1)) ≤ (((a0a2) ∩ (b0b2)) ∪ ((a1a2) ∩ (b1b2)))
 Colors of variables: term This axiom is referenced by:  dp15lemb  1155  xdp15  1199  xxdp15  1202
 Copyright terms: Public domain W3C validator