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 70  ror 71  2or 72  anass 76  or12 80  anor2 89  orordi 112  a5c 121  omlem1 127  letr 137  bltr 138  bile 142  ler 149  leror 152  lecom 180  comcom2 183  wwfh2 217  ka4lemo 228  sklem 230  skr0 242  wlem1 243  mccune3 248  i3n1 249  ri3 253  ud4lem0b 263  i3i4 270  ud4lem0c 280  wql2lem4 291  wql2lem5 292  oaidlem1 294  womle2a 295  nomcon0 301  nom13 310  nom14 311  nom15 312  nom20 313  nom22 315  nom50 331  wdf-c1 383  ska2 432  ska4 433  woml6 436  woml7 437  omlan 448  oml5 449  fh2 470  fh3rc 481  fh4rc 482  oml6 488  dfi4b 500  i3n2 501  oi3ai3 503  i3lem4 507  lem4 511  i3abs1 522  i3abs3 524  i3th1 543  i3con 551  i3orlem6 557  ud1lem2 561  ud1lem3 562  ud3lem1c 568  ud3lem1d 569  ud3lem2 571  ud3lem3c 574  ud3lem3d 575  ud3lem3 576  ud4lem1c 579  ud4lem1 581  ud4lem2 582  ud4lem3b 584  ud5lem1 589  u1lemab 610  u1lemoa 620  u2lemoa 621  u3lemoa 622  u4lemoa 623  u5lemoa 624  u1lemona 625  u2lemona 626  u3lemona 627  u4lemona 628  u5lemona 629  u1lemob 630  u2lemob 631  u3lemob 632  u4lemob 633  u5lemob 634  u1lemonb 635  u2lemonb 636  u3lemonb 637  u4lemonb 638  u5lemonb 639  u4lemnab 653  u5lemnab 654  u2lemnanb 656  u5lemnanb 659  u5lemc4 705  comi1 709  u2lemle2 716  u3lem2 746  u4lem2 747  u5lem2 748  u4lem3 752  u5lem3 753  u1lem4 757  u4lem4 759  u5lem4 760  u4lem5 764  u5lem5 765  u4lem5n 766  u3lem6 767  u4lem6 768  u5lem6 769  u24lem 770  u12lem 771  u2lem7n 775  u1lem8 776  u1lem11 780  u3lem9 784  u3lem11 786  u3lemax4 796  u3lemax5 797  bi1o1a 798  i1abs 801  test 802  3vth5 808  3vth6 809  3vth9 812  3vded21 817  3vded3 819  2oalem1 825  3vroa 831  sa5 836  orbi 842  i1orni1 847  negantlem3 850  negantlem4 851  negant0 857  negantlem9 859  neg3antlem2 865  elimcons 868  elimcons2 869  mhlemlem2 875  mhlem 876  mhlem1 877  marsdenlem2 881  mlaconjo 886  e2ast2 894  e2astlem1 895  gomaex3lem2 915  gomaex3lem3 916  oat 927  oatr 928  oau 929  oaidlem2 931  oaidlem2g 932  oa23 936  oa4to4u 973  oa4uto4g 975  oa3-2lema 978  oa3-6lem 980  oa3-3lem 981  oa3-1lem 982  oa3-5lem 984  oa3-1to5 993  d3oa 995  mloa 1018  3oa2 1024  4oaiii 1040  lem3.3.7i0e1 1057  lem3.3.7i1e1 1060  lem3.3.7i1e2 1061  lem3.3.7i2e1 1063  lem3.3.7i2e2 1064  lem3.3.7i3e1 1066  lem3.3.7i3e2 1067  lem3.3.7i4e1 1069  lem3.3.7i5e1 1072  lem4.6.2e1 1080  lem4.6.6i1j3 1092  lem4.6.6i2j4 1095  lem4.6.6i3j0 1096  lem4.6.6i3j1 1097  lem4.6.6i4j2 1099  wdwom 1104  vneulem10 1138  vneulemexp 1146

Copyright terms: Public domain