Axiom ax-r5 38

Description: Inference rule for ortholattices. (Contributed by NM, 9-Aug-1997.)

Hypothesis

Ref	Expression
r5.1	a = b

Assertion

Ref	Expression
ax-r5	(a ∪ c) = (b ∪ 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 ∪ c)
4		wvb	. . 3 term  b
5	4, 2	wo 6	. 2 term  (b ∪ c)
6	3, 5	wb 1	1 wff  (a ∪ c) = (b ∪ c)

This axiom is referenced by:  lor  70  ror  71  2or  72  anass  76  or12  80  anor2  89  orordi  112  anabs  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  1082  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  wdwom  1106  vneulem10  1140  vneulemexp  1148