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 66  con2 67  con3 68  con4 69  ancom 74  anass 76  lan 77  oran 87  anor1 88  anor2 89  dfnb 95  lbi 97  dff2 100  or0 102  oridm 110  cbtr 182  wwcomd 214  wwfh2 217  wwfh3 218  wwfh4 219  ka4lemo 228  ska3 232  skr0 242  mccune3 248  ni31 250  li3 252  ri3 253  ud1lem0b 256  ud2lem0a 258  ud2lem0b 259  ud4lem0a 262  ud4lem0b 263  ud5lem0a 264  ud5lem0b 265  ud1lem0c 277  ud2lem0c 278  ud4lem0c 280  ud5lem0c 281  wql2lem2 289  wql2lem5 292  nom50 331  nom51 332  nom52 333  nom53 334  nom54 335  k1-4 359  2vwomlem 365  wom2 434  ka4ot 435  woml6 436  woml7 437  omla 447  comcom 453  comdr 466  df2c1 468  fh2 470  fh3 471  fh4 472  gsth2 490  ni32 502  lem4 511  ud1lem2 561  ud3lem3 576  ud4lem1a 577  u1lemnaa 640  u2lemnaa 641  u3lemnaa 642  u4lemnaa 643  u5lemnaa 644  u1lemnana 645  u2lemnana 646  u4lemnana 648  u1lem1n 739  u2lem1n 740  u3lem1n 741  u4lem1n 742  u5lem1n 743  u1lem9a 777  u3lem12 788  u3lemax4 796  u3lemax5 797  3vth2 805  3vded21 817  3vded22 818  2oath1 826  salem1 837  mlaconj4 844  negantlem8 856  elimconslem 867  elimcons 868  elimcons2 869  mhlemlem2 875  mh 879  cancellem 891  gomaex3h1 902  gomaex3h2 903  gomaex3h3 904  gomaex3h4 905  gomaex3h5 906  gomaex3h6 907  gomaex3h7 908  gomaex3h8 909  gomaex3h9 910  gomaex3h10 911  gomaex3h11 912  gomaex3h12 913  gomaex3lem3 916  gomaex3lem4 917  gomaex3 924  oa23 936  oa6to4h1 955  oa6to4h2 956  oa6to4h3 957  oaliii 1001  oalem2 1006  lem3.3.4 1052  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066

Copyright terms: Public domain