ax-r4 - Quantum Logic Explorer

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

Axiom ax-r4 37

Description: Inference rule for ortholattices.

**Hypothesis**
Ref	Expression
r4.1

**Assertion**
Ref	Expression
ax-r4

**Detailed syntax breakdown of Axiom ax-r4**
Step	Hyp	Ref	Expression
1		wva	. . 3
2	1	wn 4	. 2
3		wvb	. . 3
4	3	wn 4	. 2
5	2, 4	wb 1	1

Colors of variables: term

This axiom is referenced by: con1 66 con2 67 con3 68 con4 69 ancom 74 anass 76 lan 77 oran 87 anor1 88 anor2 89 dfnb 95 lbi 97 dff2 100 or0 102 oridm 110 cbtr 182 wwcomd 214 wwfh2 217 wwfh3 218 wwfh4 219 ka4lemo 228 ska3 232 skr0 242 mccune3 248 ni31 250 li3 252 ri3 253 ud1lem0b 256 ud2lem0a 258 ud2lem0b 259 ud4lem0a 262 ud4lem0b 263 ud5lem0a 264 ud5lem0b 265 ud1lem0c 277 ud2lem0c 278 ud4lem0c 280 ud5lem0c 281 wql2lem2 289 wql2lem5 292 nom50 331 nom51 332 nom52 333 nom53 334 nom54 335 k1-4 359 2vwomlem 365 wom2 434 ka4ot 435 woml6 436 woml7 437 omla 447 comcom 453 comdr 466 df2c1 468 fh2 470 fh3 471 fh4 472 gsth2 490 ni32 502 lem4 511 ud1lem2 561 ud3lem3 576 ud4lem1a 577 u1lemnaa 640 u2lemnaa 641 u3lemnaa 642 u4lemnaa 643 u5lemnaa 644 u1lemnana 645 u2lemnana 646 u4lemnana 648 u1lem1n 739 u2lem1n 740 u3lem1n 741 u4lem1n 742 u5lem1n 743 u1lem9a 777 u3lem12 788 u3lemax4 796 u3lemax5 797 3vth2 805 3vded21 817 3vded22 818 2oath1 826 salem1 837 mlaconj4 844 negantlem8 856 elimconslem 867 elimcons 868 elimcons2 869 mhlemlem2 875 mh 879 cancellem 891 gomaex3h1 902 gomaex3h2 903 gomaex3h3 904 gomaex3h4 905 gomaex3h5 906 gomaex3h6 907 gomaex3h7 908 gomaex3h8 909 gomaex3h9 910 gomaex3h10 911 gomaex3h11 912 gomaex3h12 913 gomaex3lem3 916 gomaex3lem4 917 gomaex3 924 oa23 936 oa6to4h1 955 oa6to4h2 956 oa6to4h3 957 oaliii 1001 oalem2 1006 lem3.3.4 1053 lem3.3.7i2e2 1064 lem3.3.7i3e1 1066 lem3.3.7i3e2 1067

Copyright terms: Public domain