Axiom ax-r4 37

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 64  con2 65  con3 66  ancom 69  anass 70  lan 71  oran 81  anor1 82  anor2 83  dfnb 89  lbi 91  dff2 94  or0 96  oridm 104  cbtr 176  wwcomd 208  wwfh2 211  wwfh3 212  wwfh4 213  ka4lemo 222  ska3 226  skr0 236  mccune3 242  ni31 244  li3 246  ri3 247  ud1lem0b 250  ud2lem0a 252  ud2lem0b 253  ud4lem0a 256  ud4lem0b 257  ud5lem0a 258  ud5lem0b 259  ud1lem0c 271  ud2lem0c 272  ud4lem0c 274  ud5lem0c 275  wql2lem2 283  wql2lem5 286  nom50 325  nom51 326  nom52 327  nom53 328  nom54 329  2vwomlem 351  wom2 420  ka4ot 421  woml6 422  woml7 423  omla 433  comcom 439  comdr 452  df2c1 454  fh2 456  fh3 457  fh4 458  gsth2 476  ni32 488  lem4 497  ud1lem2 547  ud3lem3 562  ud4lem1a 563  u1lemnaa 626  u2lemnaa 627  u3lemnaa 628  u4lemnaa 629  u5lemnaa 630  u1lemnana 631  u2lemnana 632  u4lemnana 634  u1lem1n 725  u2lem1n 726  u3lem1n 727  u4lem1n 728  u5lem1n 729  u1lem9a 763  u3lem12 774  u3lemax4 782  u3lemax5 783  3vth2 791  3vded21 803  3vded22 804  2oath1 812  salem1 823  mlaconj4 830  negantlem8 842  elimconslem 853  elimcons 854  elimcons2 855  mhlemlem2 861  mh 865  cancellem 877  gomaex3h1 888  gomaex3h2 889  gomaex3h3 890  gomaex3h4 891  gomaex3h5 892  gomaex3h6 893  gomaex3h7 894  gomaex3h8 895  gomaex3h9 896  gomaex3h10 897  gomaex3h11 898  gomaex3h12 899  gomaex3lem3 902  gomaex3lem4 903  gomaex3 910  oa23 922  oa6to4h1 941  oa6to4h2 942  oa6to4h3 943  oaliii 987  oalem2 992  lem3.3.4 1038  lem3.3.7i2e2 1049  lem3.3.7i3e1 1051  lem3.3.7i3e2 1052

Copyright terms: Public domain