Axiom ax-r1 35

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

Hypothesis

Ref	Expression
r1.1	a = b

Assertion

Ref	Expression
ax-r1	b = a

Detailed syntax breakdown of Axiom ax-r1

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

This axiom is referenced by:  id  59  tt  60  cm  61  3tr1  63  3tr2  64  con2  67  anor1  88  anor2  89  anor3  90  oran1  91  oran2  92  oran3  93  dfb  94  dfnb  95  dff  101  or1  104  an1  106  oridm  110  orordi  112  orordir  113  anandi  114  anandir  115  1b  117  1bi  119  leoa  123  leao  124  di  126  omlem1  127  omlem2  128  letr  137  lbtr  139  le3tr1  140  le3tr2  141  qlhoml1b  144  lebi  145  ler  149  leror  152  leran  153  ler2or  172  ler2an  173  ledi  174  ledio  176  comm0  178  comm1  179  lecom  180  wr3  198  wr4  199  wwbmp  205  wcon2  208  wcon3  209  wlem3.1  210  wwoml2  212  wwoml3  213  wwcomd  214  wwcom3ii  215  wwfh1  216  wwfh2  217  wwfh4  219  ka4lemo  228  ka4lem  229  sklem  230  ska6  234  ska8  236  skr0  242  wlem1  243  mccune2  247  mccune3  248  i3n1  249  ni31  250  i3id  251  i1i2con1  268  i1i2con2  269  i4i3  271  1i1  274  i2id  276  ud1lem0c  277  ud2lem0c  278  ud4lem0c  280  ud5lem0c  281  wql1lem  287  wql2lem2  289  wql2lem3  290  wql2lem4  291  wql1  293  womle2b  296  womle3b  297  womle  298  nom11  308  nom12  309  nom13  310  nom14  311  nom15  312  nom20  313  nom21  314  nom22  315  nom23  316  nom24  317  nom25  318  nom31  320  nom32  321  nom40  325  nom41  326  nom42  327  nom43  328  nom44  329  nom45  330  nom50  331  nom51  332  nom52  333  nom53  334  nom54  335  nom55  336  nom61  338  nom62  339  go1  343  i2or  344  i1or  345  k1-2  357  k1-3  358  2vwomr2  362  2vwomr1a  363  2vwomr2a  364  2vwomlem  365  wr5-2v  366  wom3  367  wdf-le2  379  wdf-c2  384  wler  391  wcom2an  428  wlem14  430  ska2  432  ska4  433  wom2  434  woml6  436  woml7  437  ortha  438  lem3.1  443  lem3a.1  444  omla  447  oml3  452  comcom  453  comd  456  com3ii  457  df2c1  468  fh1  469  fh2  470  fh3  471  fh4  472  com2or  483  com2an  484  combi  485  oml4  487  oml6  488  gsth  489  gsth2  490  gstho  491  cmtr1com  493  comcmtr1  494  i0cmtrcom  495  i3bi  496  i3or  497  dfi3b  499  dfi4b  500  i3n2  501  ni32  502  oi3ai3  503  i3lem1  504  i3lem2  505  i3lem3  506  i3lem4  507  comi31  508  com2i3  509  lem4  511  i3i0  513  ska14  514  bii3  516  i3abs3  524  i33tr1  529  i33tr2  530  i3th1  543  i3th4  546  i3th7  549  i3th8  550  i3con  551  i3orlem1  552  i3orlem3  554  i3orlem4  555  i3orlem5  556  i3orlem6  557  i3orlem7  558  i3orlem8  559  ud1lem1  560  ud1lem2  561  ud1lem3  562  ud2lem1  563  ud2lem2  564  ud2lem3  565  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem1  570  ud3lem2  571  ud3lem3b  573  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem2  582  ud4lem3b  584  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1c  588  ud5lem1  589  ud5lem2  590  ud5lem3a  591  ud5lem3b  592  ud5lem3c  593  ud5lem3  594  ud1  595  ud2  596  ud3  597  ud4  598  ud5  599  u1lemaa  600  u2lemaa  601  u3lemaa  602  u4lemaa  603  u5lemaa  604  u3lemana  607  u4lemana  608  u5lemana  609  u3lemab  612  u4lemab  613  u5lemab  614  u1lemanb  615  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u1lemoa  620  u2lemoa  621  u4lemoa  623  u5lemoa  624  u4lemona  628  u3lemob  632  u4lemob  633  u1lemonb  635  u2lemonb  636  u3lemonb  637  u1lemnaa  640  u2lemnaa  641  u3lemnaa  642  u4lemnaa  643  u5lemnaa  644  u1lemnana  645  u2lemnana  646  u4lemnana  648  u1lemnab  650  u2lemnab  651  u3lemnab  652  u1lemnoa  660  u2lemnonb  676  u1lemc1  680  u2lemc1  681  u4lemc1  683  u5lemc1  684  u5lemc1b  685  u1lemc2  686  u2lemc2  687  u4lemc2  689  u5lemc2  690  u1lemc4  701  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  comi12  707  u1lemle2  715  u2lemle2  716  u4lemle2  718  u5lemle2  719  u1lembi  720  u2lembi  721  i2bi  722  u4lembi  724  u5lembi  725  u12lembi  726  u1lemn1b  730  u1lem3var1  731  u2lem1  735  u3lem1n  741  u4lem1n  742  u5lem1n  743  u1lem2  744  u2lem2  745  u1lem3  749  u2lem3  750  u1lem4  757  u4lem4  759  u5lem4  760  u1lem5  761  u4lem5  764  u5lem5  765  u3lem6  767  u4lem6  768  u5lem6  769  u24lem  770  u1lem7  772  u2lem7  773  u3lem7  774  u1lem8  776  u1lem9a  777  u1lem9b  778  u1lem11  780  u2lem8  782  u3lem8  783  u3lem9  784  u3lem10  785  u3lem11  786  u3lem12  788  u3lem13a  789  u3lem13b  790  u3lem14a  791  u3lem14aa2  793  u3lem14mp  794  u3lem15  795  u3lemax4  796  u3lemax5  797  bi1o1a  798  biao  799  i2i1i1  800  i1abs  801  test  802  test2  803  3vth1  804  3vth5  808  3vth6  809  3vth7  810  3vth8  811  3vth9  812  3vcom  813  3vded11  814  3vded12  815  3vded13  816  3vded21  817  3vded22  818  3vded3  819  1oa  820  1oai1  821  2oai1u  822  1oaiii  823  2oalem1  825  2oath1  826  2oath1i1  827  1oath1i1u  828  oale  829  3vroa  831  mlalem  832  sa5  836  salem1  837  sadm3  838  bi3  839  bi4  840  orbi  842  mlaconj4  844  i1orni1  847  negantlem1  848  negantlem2  849  negantlem3  850  negantlem4  851  negant  852  negantlem9  859  negant3  860  negantlem10  861  negant4  862  neg3antlem1  864  neg3antlem2  865  neg3ant1  866  elimconslem  867  elimcons  868  elimcons2  869  comanblem1  870  comanblem2  871  comanbn  873  mhlem  876  mhlem1  877  mh  879  marsdenlem2  881  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  oago3.29  889  oago3.21x  890  cancellem  891  cancel  892  e2ast2  894  govar  896  govar2  897  go2n4  899  go2n6  901  gomaex3h7  908  gomaex3h10  911  gomaex3lem1  914  gomaex3lem2  915  gomaex3lem3  916  gomaex3lem4  917  gomaex3lem7  920  gomaex3lem9  922  gomaex3  924  oas  925  oat  927  oatr  928  oau  929  oaidlem2  931  oaidlem2g  932  oa23  936  distoah2  941  distoah3  942  distoa  944  oa3to4lem1  945  oa3to4lem2  946  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4btoc  966  oa4to4u  973  oa4gto4u  976  oa3-6lem  980  oa3-3lem  981  oa3-4lem  983  oa3-u1lem  985  oa3-u2lem  986  oa3-6to3  987  oa3-2to4  988  oa3-2to2s  990  oa3-u1  991  oa3-u2  992  d3oa  995  d4oa  996  oal2  999  oaliii  1001  oaliv  1003  oath1  1004  oalem1  1005  oadist2a  1007  oadist2b  1008  oagen1b  1015  mloa  1018  oadist  1019  oadistb  1020  oadistc0  1021  oadistc  1022  oadistd  1023  oa3moa3  1029  axoa4a  1037  axoa4d  1038  4oath1  1041  4oagen1  1042  4oagen1b  1043  4oadist  1044  lem3.3.2  1046  lem3.3.4  1053  lem3.3.5  1055  lem3.3.6  1056  lem3.3.7i0e1  1057  lem3.3.7i1e1  1060  lem3.3.7i1e2  1061  lem3.3.7i2e1  1063  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e1  1069  lem3.3.7i4e2  1070  lem3.3.7i5e1  1072  lem3.3.7i5e2  1073  lem3.4.3  1076  lem3.4.4  1077  lem3.4.6  1079  lem4.6.2e1  1082  lem4.6.5  1087  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  lem4.6.7  1103  wdcom  1105  wdwom  1106  wdid0id5  1111  wdid0id1  1112  wdid0id2  1113  wdid0id3  1114  wdid0id4  1115  mldual  1124