lel2or - Quantum Logic Explorer

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

Theorem lel2or 170

Description: Disjunction of 2 l.e.'s.

**Hypotheses**
Ref	Expression
lel2.1
lel2.2

**Assertion**
Ref	Expression
lel2or

**Proof of Theorem lel2or**
Step	Hyp	Ref	Expression
1		lel2.1	. . 3
2		lel2.2	. . 3
3	1, 2	le2or 168	. 2
4		oridm 110	. 2
5	3, 4	lbtr 139	1

Colors of variables: term

Syntax hints:

wle 2

wo 6

This theorem was proved from axioms: ax-a1 30 ax-a2 31 ax-a3 32 ax-a5 34 ax-r1 35 ax-r2 36 ax-r4 37 ax-r5 38

This theorem depends on definitions: df-a 40 df-t 41 df-f 42 df-le1 130 df-le2 131

This theorem is referenced by: womao 220 womaon 221 womaa 222 womaan 223 anorabs2 224 mccune2 247 nom14 311 i2or 344 i1or 345 i5lei1 347 i5lei2 348 k1-2 357 k1-3 358 wdf-c2 384 cmtr1com 493 i0cmtrcom 495 ud3lem1c 568 ud3lem3 576 ud4lem1c 579 ud4lem1 581 ud5lem1 589 u3lemana 607 u4lemab 613 u5lemab 614 u3lemona 627 u4lemona 628 u5lemona 629 u4lemob 633 u5lemob 634 i2bi 722 u4lem1 737 u4lem5 764 u4lem6 768 u12lem 771 u3lem13a 789 u3lem13b 790 3vded11 814 3vded12 815 3vded22 818 1oa 820 mlalem 832 sa5 836 sadm3 838 negantlem2 849 negantlem4 851 negantlem9 859 negantlem10 861 neg3antlem2 865 neg3ant1 866 mhlem2 878 mh 879 cancellem 891 kb10iii 893 gomaex3lem2 915 oas 925 oatr 928 oaur 930 oal42 935 oa3to4lem4 948 oa4b 959 oa4to4u2 974 oa3-u1lem 985 oa3-u1 991 oa3-u2 992 oa3-1to5 993 d4oa 996 oadist2b 1008 mloa 1018 oa3moa3 1029 lem3.3.7i4e1 1069 lem4.6.6i0j1 1086 lem4.6.6i0j2 1087 lem4.6.6i0j3 1088 lem4.6.6i0j4 1089 lem4.6.6i1j3 1092 lem4.6.6i2j0 1093 lem4.6.6i2j1 1094 lem4.6.6i2j4 1095 lem4.6.6i3j0 1096 lem4.6.6i3j1 1097 lem4.6.6i4j0 1098 lem4.6.6i4j2 1099 lem4.6.7 1101 ml 1121 ml3le 1127 vneulem6 1134 vneulemexp 1146 dp53lema 1161 dp53lemf 1166 dp35lemf 1170 dp35lemd 1172 dp35lema 1176 dp41lemc 1183 xdp41 1196 xdp53 1198 xxdp41 1199 xxdp53 1201 xdp45lem 1202 xdp43lem 1203 xdp45 1204 xdp43 1205 3dp43 1206 oadp35lemf 1208