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

Theorem i3i4 270
 Description: Correspondence between Kalmbach and non-tollens conditionals.
Assertion
Ref Expression
i3i4 (a3 b) = (b4 a )

Proof of Theorem i3i4
StepHypRef Expression
1 ax-a2 31 . . . 4 ((ab) ∪ (ab )) = ((ab ) ∪ (ab))
2 ancom 74 . . . . 5 (ab ) = (ba )
3 ancom 74 . . . . . 6 (ab) = (ba )
4 ax-a1 30 . . . . . . 7 b = b
54ran 78 . . . . . 6 (ba ) = (b a )
63, 5ax-r2 36 . . . . 5 (ab) = (b a )
72, 62or 72 . . . 4 ((ab ) ∪ (ab)) = ((ba ) ∪ (b a ))
81, 7ax-r2 36 . . 3 ((ab) ∪ (ab )) = ((ba ) ∪ (b a ))
9 ancom 74 . . . 4 (a ∩ (ab)) = ((ab) ∩ a)
10 ax-a2 31 . . . . . 6 (ab) = (ba )
114ax-r5 38 . . . . . 6 (ba ) = (b a )
1210, 11ax-r2 36 . . . . 5 (ab) = (b a )
13 ax-a1 30 . . . . 5 a = a
1412, 132an 79 . . . 4 ((ab) ∩ a) = ((b a ) ∩ a )
159, 14ax-r2 36 . . 3 (a ∩ (ab)) = ((b a ) ∩ a )
168, 152or 72 . 2 (((ab) ∪ (ab )) ∪ (a ∩ (ab))) = (((ba ) ∪ (b a )) ∪ ((b a ) ∩ a ))
17 df-i3 46 . 2 (a3 b) = (((ab) ∪ (ab )) ∪ (a ∩ (ab)))
18 df-i4 47 . 2 (b4 a ) = (((ba ) ∪ (b a )) ∪ ((b a ) ∩ a ))
1916, 17, 183tr1 63 1 (a3 b) = (b4 a )
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →3 wi3 14   →4 wi4 15 This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38 This theorem depends on definitions:  df-a 40  df-i3 46  df-i4 47 This theorem is referenced by:  i4i3  271  nom43  328
 Copyright terms: Public domain W3C validator