Axiom ax-r2 36

Description: Inference rule for ortholattices.

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  a5b 120  a5c 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 1036  4oaiii 1039  4oath1 1040  4oagen1 1041  4oagen1b 1042  4oadist 1043  lem3.3.2 1045  lem3.3.4 1052  lem3.3.6 1055  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e2 1069  lem3.4.1 1074  lem3.4.4 1076  lem3.4.6 1078  lem4.6.6i1j3 1091  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  com3iia 1099  lem4.6.7 1100  wdcom 1102  wdwom 1103  wdid0id5 1108  wdid0id1 1109  wdid0id2 1110  wdid0id3 1111  wdid0id4 1112

Copyright terms: Public domain