Axiom ax-r5 38

Description: Inference rule for ortholattices.

Hypothesis

Ref	Expression
r5.1	a = b

Assertion

Ref	Expression
ax-r5	(a v c) = (b v c)

Detailed syntax breakdown of Axiom ax-r5

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvc	. . 3 term c
3	1, 2	wo 6	. 2 term (a v c)
4		wvb	. . 3 term b
5	4, 2	wo 6	. 2 term (b v c)
6	3, 5	wb 1	1 wff (a v c) = (b v c)

This axiom is referenced by:  lor 67  2or 68  anass 70  or12 74  anor2 83  orordi 106  a5c 115  omlem1 121  letr 131  bltr 132  bile 136  ler 143  leror 146  lecom 174  comcom2 177  wwfh2 211  ka4lemo 222  sklem 224  skr0 236  wlem1 237  mccune3 242  i3n1 243  ri3 247  ud4lem0b 257  i3i4 264  ud4lem0c 274  wql2lem4 285  wql2lem5 286  oaidlem1 288  womle2a 289  nomcon0 295  nom13 304  nom14 305  nom15 306  nom20 307  nom22 309  nom50 325  wdf-c1 369  ska2 418  ska4 419  woml6 422  woml7 423  omlan 434  oml5 435  fh2 456  fh3rc 467  fh4rc 468  oml6 474  dfi4b 486  i3n2 487  oi3ai3 489  i3lem4 493  lem4 497  i3abs1 508  i3abs3 510  i3th1 529  i3con 537  i3orlem6 543  ud1lem2 547  ud1lem3 548  ud3lem1c 554  ud3lem1d 555  ud3lem2 557  ud3lem3c 560  ud3lem3d 561  ud3lem3 562  ud4lem1c 565  ud4lem1 567  ud4lem2 568  ud4lem3b 570  ud5lem1 575  u1lemab 596  u1lemoa 606  u2lemoa 607  u3lemoa 608  u4lemoa 609  u5lemoa 610  u1lemona 611  u2lemona 612  u3lemona 613  u4lemona 614  u5lemona 615  u1lemob 616  u2lemob 617  u3lemob 618  u4lemob 619  u5lemob 620  u1lemonb 621  u2lemonb 622  u3lemonb 623  u4lemonb 624  u5lemonb 625  u4lemnab 639  u5lemnab 640  u2lemnanb 642  u5lemnanb 645  u5lemc4 691  comi1 695  u2lemle2 702  u3lem2 732  u4lem2 733  u5lem2 734  u4lem3 738  u5lem3 739  u1lem4 743  u4lem4 745  u5lem4 746  u4lem5 750  u5lem5 751  u4lem5n 752  u3lem6 753  u4lem6 754  u5lem6 755  u24lem 756  u12lem 757  u2lem7n 761  u1lem8 762  u1lem11 766  u3lem9 770  u3lem11 772  u3lemax4 782  u3lemax5 783  bi1o1a 784  i1abs 787  test 788  3vth5 794  3vth6 795  3vth9 798  3vded21 803  3vded3 805  2oalem1 811  3vroa 817  sa5 822  orbi 828  i1orni1 833  negantlem3 836  negantlem4 837  negant0 843  negantlem9 845  neg3antlem2 851  elimcons 854  elimcons2 855  mhlemlem2 861  mhlem 862  mhlem1 863  marsdenlem2 867  mlaconjo 872  e2ast2 880  e2astlem1 881  gomaex3lem2 901  gomaex3lem3 902  oat 913  oatr 914  oau 915  oaidlem2 917  oaidlem2g 918  oa23 922  oa4to4u 959  oa4uto4g 961  oa3-2lema 964  oa3-6lem 966  oa3-3lem 967  oa3-1lem 968  oa3-5lem 970  oa3-1to5 979  d3oa 981  mloa 1004  3oa2 1010  4oaiii 1025  lem3.3.7i0e1 1042  lem3.3.7i1e1 1045  lem3.3.7i1e2 1046  lem3.3.7i2e1 1048  lem3.3.7i2e2 1049  lem3.3.7i3e1 1051  lem3.3.7i3e2 1052  lem3.3.7i4e1 1054  lem3.3.7i5e1 1057  lem4.6.2e1 1065  lem4.6.6i1j3 1077  lem4.6.6i2j4 1080  lem4.6.6i3j0 1081  lem4.6.6i3j1 1082  lem4.6.6i4j2 1084  wdwom 1089

Copyright terms: Public domain