Axiom ax-r5 37

Description: Inference rule for ortholattices.

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 66  2or 67  anass 69  or12 73  anor2 81  orordi 104  a5c 113  omlem1 119  letr 129  bltr 130  bile 134  ler 141  leror 144  lecom 172  comcom2 175  wwfh2 209  ka4lemo 220  sklem 222  skr0 234  wlem1 235  mccune3 240  i3n1 241  ri3 245  ud4lem0b 255  i3i4 262  ud4lem0c 272  wql2lem4 283  wql2lem5 284  oaidlem1 286  womle2a 287  nomcon0 293  nom13 302  nom14 303  nom15 304  nom20 305  nom22 307  nom50 323  wdf-c1 365  ska2 414  ska4 415  woml6 418  woml7 419  omlan 430  oml5 431  fh2 452  fh3rc 463  fh4rc 464  oml6 470  dfi4b 482  i3n2 483  oi3ai3 485  i3lem4 489  lem4 493  i3abs1 504  i3abs3 506  i3th1 525  i3con 533  i3orlem6 539  ud1lem2 543  ud1lem3 544  ud3lem1c 550  ud3lem1d 551  ud3lem2 553  ud3lem3c 556  ud3lem3d 557  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud4lem2 564  ud4lem3b 566  ud5lem1 571  u1lemab 592  u1lemoa 602  u2lemoa 603  u3lemoa 604  u4lemoa 605  u5lemoa 606  u1lemona 607  u2lemona 608  u3lemona 609  u4lemona 610  u5lemona 611  u1lemob 612  u2lemob 613  u3lemob 614  u4lemob 615  u5lemob 616  u1lemonb 617  u2lemonb 618  u3lemonb 619  u4lemonb 620  u5lemonb 621  u4lemnab 635  u5lemnab 636  u2lemnanb 638  u5lemnanb 641  u5lemc4 687  comi1 691  u2lemle2 698  u3lem2 728  u4lem2 729  u5lem2 730  u4lem3 734  u5lem3 735  u1lem4 739  u4lem4 741  u5lem4 742  u4lem5 746  u5lem5 747  u4lem5n 748  u3lem6 749  u4lem6 750  u5lem6 751  u24lem 752  u12lem 753  u2lem7n 757  u1lem8 758  u1lem11 762  u3lem9 766  u3lem11 768  u3lemax4 778  u3lemax5 779  bi1o1a 780  i1abs 783  test 784  3vth5 790  3vth6 791  3vth9 794  3vded21 799  3vded3 801  2oalem1 807  3vroa 813  sa5 818  orbi 824  i1orni1 829  negantlem3 832  negantlem4 833  negant0 839  negantlem9 841  neg3antlem2 847  elimcons 850  elimcons2 851  mhlemlem2 857  mhlem 858  mhlem1 859  marsdenlem2 863  mlaconjo 868  gomaex3lem2 895  gomaex3lem3 896  oat 907  oatr 908  oau 909  oaidlem2 911  oaidlem2g 912  oa23 916  oa4to4u 953  oa4uto4g 955  oa3-2lema 958  oa3-6lem 960  oa3-3lem 961  oa3-1lem 962  oa3-5lem 964  oa3-1to5 973  d3oa 975  mloa 998  3oa2 1004  4oaiii 1019

metamath.org