Axiom ax-r4 36

Description: Inference rule for ortholattices.

Hypothesis

Ref	Expression
r4.1	a = b

Assertion

Ref	Expression
ax-r4	a⊥ = b⊥

Detailed syntax breakdown of Axiom ax-r4

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2	1	wn 4	. 2 term  a⊥
3		wvb	. . 3 term  b
4	3	wn 4	. 2 term  b⊥
5	2, 4	wb 1	1 wff  a⊥ = b⊥

This axiom is referenced by:  con1 63  con2 64  con3 65  ancom 68  anass 69  lan 70  oran 79  anor1 80  anor2 81  dfnb 87  lbi 89  dff2 92  or0 94  oridm 102  cbtr 174  wwcomd 206  wwfh2 209  wwfh3 210  wwfh4 211  ka4lemo 220  ska3 224  skr0 234  mccune3 240  ni31 242  li3 244  ri3 245  ud1lem0b 248  ud2lem0a 250  ud2lem0b 251  ud4lem0a 254  ud4lem0b 255  ud5lem0a 256  ud5lem0b 257  ud1lem0c 269  ud2lem0c 270  ud4lem0c 272  ud5lem0c 273  wql2lem2 281  wql2lem5 284  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  2vwomlem 347  wom2 416  ka4ot 417  woml6 418  woml7 419  omla 429  comcom 435  comdr 448  df2c1 450  fh2 452  fh3 453  fh4 454  gsth2 472  ni32 484  lem4 493  ud1lem2 543  ud3lem3 558  ud4lem1a 559  u1lemnaa 622  u2lemnaa 623  u3lemnaa 624  u4lemnaa 625  u5lemnaa 626  u1lemnana 627  u2lemnana 628  u4lemnana 630  u1lem1n 721  u2lem1n 722  u3lem1n 723  u4lem1n 724  u5lem1n 725  u1lem9a 759  u3lem12 770  u3lemax4 778  u3lemax5 779  3vth2 787  3vded21 799  3vded22 800  2oath1 808  salem1 819  mlaconj4 826  negantlem8 838  elimconslem 849  elimcons 850  elimcons2 851  mhlemlem2 857  mh 861  cancellem 873  gomaex3h1 882  gomaex3h2 883  gomaex3h3 884  gomaex3h4 885  gomaex3h5 886  gomaex3h6 887  gomaex3h7 888  gomaex3h8 889  gomaex3h9 890  gomaex3h10 891  gomaex3h11 892  gomaex3h12 893  gomaex3lem3 896  gomaex3lem4 897  gomaex3 904  oa23 916  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937  oaliii 981  oalem2 986

metamath.org