le3tr1 - Quantum Logic Explorer

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

Theorem le3tr1 140

Description: Transitive inference useful for introducing definitions.

**Assertion**
Ref	Expression
le3tr1

**Proof of Theorem le3tr1**
Step	Hyp	Ref	Expression
1		le3tr1.2	. . 3
2		le3tr1.1	. . 3
3	1, 2	bltr 138	. 2
4		le3tr1.3	. . 3
5	4	ax-r1 35	. 2
6	3, 5	lbtr 139	1

Colors of variables: term

Syntax hints:

wb 1

wle 2

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

This theorem depends on definitions: df-a 40 df-le1 130 df-le2 131

This theorem is referenced by: le3tr2 141 lecon1 155 lelor 166 lelan 167 ledir 175 ledior 177 ka4lemo 228 ska13 241 i5lei1 347 i5lei2 348 i5lei3 349 i5lei4 350 id5leid0 351 wdf-c2 384 i3bi 496 i3th5 547 i3orlem5 556 ud4lem1a 577 u1lemc6 706 comi1 709 i2bi 722 u3lem14mp 794 3vth1 804 1oa 820 1oai1 821 mlalem 832 sa5 836 sadm3 838 bi3 839 negantlem2 849 negantlem3 850 negantlem9 859 negantlem10 861 neg3antlem2 865 comanb 872 mhlemlem2 875 mh 879 mlaconjo 886 cancellem 891 gomaex4 900 gomaex3h1 902 gomaex3h2 903 gomaex3h3 904 gomaex3h4 905 gomaex3h5 906 gomaex3h6 907 gomaex3h7 908 gomaex3h8 909 gomaex3h9 910 gomaex3h10 911 gomaex3h11 912 gomaex3h12 913 oa23 936 oa4lem1 937 oa4lem2 938 distoah4 943 oa3to4lem5 949 oa6todual 952 oa6fromdual 953 oa8todual 971 oal2 999 oal1 1000 oa3moa3 1029 lem3.3.3lem1 1049 lem3.3.3lem2 1050 lem3.3.5 1055 lem3.4.3 1076