Axiom ax-r4 37

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

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  1053  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067