Axiom ax-r2 36

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

Hypotheses

Ref	Expression
r2.1	a = b
r2.2	b = c

Assertion

Ref	Expression
ax-r2	a = c

Detailed syntax breakdown of Axiom ax-r2

Step	Hyp	Ref	Expression
1		wva	. 2 term  a
2		wvc	. 2 term  c
3	1, 2	wb 1	1 wff  a = c

This axiom is referenced by:  id  59  tt  60  tr  62  3tr1  63  3tr  65  con2  67  con3  68  2or  72  2an  79  or42  85  anor1  88  anor2  89  dfb  94  dfnb  95  2bi  99  dff2  100  dff  101  or0  102  or0r  103  or1  104  or1r  105  an1  106  an1r  107  an0  108  an0r  109  oridm  110  anidm  111  orordi  112  orordir  113  anandi  114  anandir  115  1b  117  bi1  118  orabs  120  anabs  121  conb  122  leoa  123  leao  124  mi  125  di  126  omlem1  127  letr  137  bltr  138  lbtr  139  bile  142  lebi  145  le0  147  ler  149  lel  151  leror  152  leran  153  lea  160  comm0  178  comm1  179  lecom  180  cbtr  182  comcom2  183  cmtrcom  190  wr1  197  wr3  198  wr4  199  wwbmp  205  wcon1  207  wcon2  208  wcon3  209  wlem3.1  210  wwoml3  213  wwcomd  214  wwcom3ii  215  wwfh1  216  wwfh2  217  wwfh3  218  wwfh4  219  ka4lemo  228  ka4lem  229  sklem  230  ska8  236  skr0  242  wlem1  243  lei3  246  mccune2  247  mccune3  248  i3n1  249  ni31  250  i3id  251  2i3  254  ud1lem0ab  257  i1i2  266  i1i2con1  268  i1i2con2  269  i3i4  270  i4i3  271  i5con  272  0i1  273  1i1  274  i1id  275  i2id  276  ud1lem0c  277  ud2lem0c  278  ud4lem0c  280  ud5lem0c  281  wql2lem2  289  wql2lem3  290  wql2lem5  292  wql1  293  oaidlem1  294  womle2a  295  nomcon0  301  nomcon1  302  nomcon2  303  nomcon5  306  nom11  308  nom12  309  nom13  310  nom14  311  nom15  312  nom20  313  nom21  314  nom22  315  nom23  316  nom24  317  nom25  318  nom30  319  nom31  320  nom32  321  nom33  322  nom34  323  nom35  324  nom40  325  nom41  326  nom42  327  nom43  328  nom44  329  nom45  330  nom50  331  nom51  332  nom52  333  nom53  334  nom54  335  nom55  336  nom60  337  nom61  338  nom62  339  nom63  340  nom64  341  nom65  342  go1  343  i5lei1  347  i5lei3  349  k1-2  357  k1-3  358  2vwomr2  362  2vwomr1a  363  2vwomr2a  364  2vwomlem  365  wr5-2v  366  wlor  368  wran  369  wlan  370  wr2  371  wdf-le1  378  wdf-le2  379  wdf-c1  383  wdf-c2  384  wle0  390  wler  391  wcomcom  414  ska2  432  ska4  433  wom2  434  ka4ot  435  woml6  436  woml7  437  wed  441  r3b  442  lem3a.1  444  omln  446  omla  447  omlan  448  oml5  449  oml5a  450  oml3  452  comcom  453  comd  456  com3ii  457  comdr  466  com3i  467  df2c1  468  fh1  469  fh2  470  fh3  471  fh4  472  com2or  483  nbdi  486  oml4  487  oml6  488  gsth  489  gsth2  490  i0cmtrcom  495  i3bi  496  df2i3  498  dfi3b  499  dfi4b  500  i3n2  501  ni32  502  oi3ai3  503  i3lem1  504  i3lem3  506  i3lem4  507  lem4  511  i0i3  512  i3i0  513  ska14  514  i31  520  i3abs1  522  i3abs3  524  i3th1  543  i3th2  544  i3th3  545  i3th7  549  i3th8  550  i3con  551  i3orlem3  554  i3orlem5  556  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  ud3lem3c  574  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem2  582  ud4lem3a  583  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  u1lemana  605  u2lemana  606  u3lemana  607  u4lemana  608  u5lemana  609  u1lemab  610  u2lemab  611  u3lemab  612  u4lemab  613  u5lemab  614  u1lemanb  615  u2lemanb  616  u3lemanb  617  u4lemanb  618  u5lemanb  619  u1lemoa  620  u2lemoa  621  u3lemoa  622  u4lemoa  623  u5lemoa  624  u1lemona  625  u2lemona  626  u3lemona  627  u4lemona  628  u5lemona  629  u1lemob  630  u2lemob  631  u3lemob  632  u4lemob  633  u5lemob  634  u1lemonb  635  u2lemonb  636  u3lemonb  637  u4lemonb  638  u5lemonb  639  u1lemnaa  640  u2lemnaa  641  u3lemnaa  642  u4lemnaa  643  u5lemnaa  644  u1lemnana  645  u2lemnana  646  u3lemnana  647  u4lemnana  648  u5lemnana  649  u4lemnab  653  u5lemnab  654  u2lemnanb  656  u5lemnanb  659  u1lemnoa  660  u2lemnoa  661  u3lemnoa  662  u4lemnoa  663  u5lemnoa  664  u3lemnona  667  u4lemnob  673  u1lemnonb  675  u2lemnonb  676  u3lemnonb  677  u4lemnonb  678  u5lemnonb  679  u1lemc4  701  u2lemc4  702  u3lemc4  703  u4lemc4  704  u5lemc4  705  i1com  708  comi1  709  u1lemle1  710  u2lemle1  711  u3lemle1  712  u4lemle1  713  u5lemle1  714  u1lemle2  715  u2lemle2  716  u4lemle2  718  u5lemle2  719  u1lembi  720  u2lembi  721  u4lembi  724  u5lembi  725  u12lembi  726  oi3oa3  733  u1lem1  734  u2lem1  735  u3lem1  736  u4lem1  737  u5lem1  738  u3lem1n  741  u4lem1n  742  u5lem1n  743  u1lem2  744  u2lem2  745  u3lem2  746  u4lem2  747  u5lem2  748  u1lem3  749  u2lem3  750  u3lem3  751  u4lem3  752  u5lem3  753  u3lem3n  754  u4lem3n  755  u5lem3n  756  u1lem4  757  u3lem4  758  u4lem4  759  u5lem4  760  u1lem5  761  u2lem5  762  u3lem5  763  u4lem5  764  u5lem5  765  u4lem5n  766  u3lem6  767  u4lem6  768  u5lem6  769  u24lem  770  u12lem  771  u1lem7  772  u2lem7  773  u3lem7  774  u2lem7n  775  u1lem8  776  u1lem9a  777  u1lem11  780  u1lem12  781  u2lem8  782  u3lem8  783  u3lem9  784  u3lem10  785  u3lem11  786  u3lem11a  787  u3lem12  788  u3lem13a  789  u3lem13b  790  u3lem14a  791  u3lem14aa  792  u3lem14aa2  793  u3lem15  795  u3lemax4  796  u3lemax5  797  bi1o1a  798  biao  799  i2i1i1  800  i1abs  801  test  802  test2  803  3vth1  804  3vth3  806  3vth5  808  3vth6  809  3vth7  810  3vth8  811  3vth9  812  3vded11  814  3vded12  815  3vded13  816  3vded21  817  3vded22  818  3vded3  819  1oa  820  2oai1u  822  1oaiii  823  1oaii  824  2oalem1  825  2oath1  826  2oath1i1  827  1oath1i1u  828  oale  829  3vroa  831  mlalem  832  sa5  836  salem1  837  bi3  839  bi4  840  imp3  841  orbi  842  mlaconj4  844  mlaconj  845  i1orni1  847  negantlem1  848  negantlem2  849  negantlem3  850  negantlem4  851  negantlem9  859  negantlem10  861  neg3antlem1  864  neg3antlem2  865  elimconslem  867  elimcons2  869  comanblem1  870  comanblem2  871  comanb  872  mhlemlem1  874  mhlemlem2  875  mhlem  876  mhlem1  877  mhlem2  878  mh  879  marsdenlem1  880  marsdenlem2  881  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  cancellem  891  e2ast2  894  e2astlem1  895  govar  896  go2n4  899  gomaex4  900  go2n6  901  gomaex3h10  911  gomaex3lem2  915  gomaex3lem3  916  gomaex3lem7  920  gomaex3  924  oas  925  oat  927  oatr  928  oau  929  oaur  930  oaidlem2  931  oaidlem2g  932  oa6v4v  933  oa4v3v  934  oal42  935  oa23  936  distoah4  943  distoa  944  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem6  950  oa6todual  952  oa6fromdual  953  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa8todual  971  oa4to4u  973  oa4uto4g  975  oa4gto4u  976  oa3-2lema  978  oa3-2lemb  979  oa3-6lem  980  oa3-3lem  981  oa3-1lem  982  oa3-5lem  984  oa3-u2lem  986  oa3-6to3  987  oa3-2to4  988  oa3-2to2s  990  oa3-u1  991  oa3-u2  992  oa3-1to5  993  d3oa  995  d4oa  996  oaliii  1001  oalii  1002  oaliv  1003  oalem1  1005  oalem2  1006  oadist2a  1007  oacom  1011  oagen1  1014  oagen1b  1015  mloa  1018  oadist  1019  oadistb  1020  oadistc0  1021  oadistc  1022  oadistd  1023  3oa2  1024  axoa4a  1037  4oaiii  1040  4oath1  1041  4oagen1  1042  4oagen1b  1043  4oadist  1044  lem3.3.2  1046  lem3.3.4  1053  lem3.3.6  1056  lem3.3.7i2e2  1064  lem3.3.7i3e1  1066  lem3.3.7i3e2  1067  lem3.3.7i4e2  1070  lem3.4.1  1075  lem3.4.4  1077  lem3.4.6  1079  lem4.6.6i1j3  1094  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j2  1101  com3iia  1102  lem4.6.7  1103  wdcom  1105  wdwom  1106  wdid0id5  1111  wdid0id1  1112  wdid0id2  1113  wdid0id3  1114  wdid0id4  1115  vneulem6  1136  vneulem9  1139  vneulemexp  1148