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  3tr1 61  3tr 63  con2 65  con3 66  2or 68  2an 73  or42 79  anor1 82  anor2 83  dfb 88  dfnb 89  2bi 93  dff2 94  dff 95  or0 96  or0r 97  or1 98  or1r 99  an1 100  an1r 101  an0 102  an0r 103  oridm 104  anidm 105  orordi 106  orordir 107  anandi 108  anandir 109  1b 111  bi1 112  a5b 114  a5c 115  conb 116  leoa 117  leao 118  mi 119  di 120  omlem1 121  letr 131  bltr 132  lbtr 133  bile 136  lebi 139  le0 141  ler 143  lel 145  leror 146  leran 147  lea 154  comm0 172  comm1 173  lecom 174  cbtr 176  comcom2 177  cmtrcom 184  wr1 191  wr3 192  wr4 193  wwbmp 199  wcon1 201  wcon2 202  wcon3 203  wlem3.1 204  wwoml3 207  wwcomd 208  wwcom3ii 209  wwfh1 210  wwfh2 211  wwfh3 212  wwfh4 213  ka4lemo 222  ka4lem 223  sklem 224  ska8 230  skr0 236  wlem1 237  lei3 240  mccune2 241  mccune3 242  i3n1 243  ni31 244  i3id 245  2i3 248  ud1lem0ab 251  i1i2 260  i1i2con1 262  i1i2con2 263  i3i4 264  i4i3 265  i5con 266  0i1 267  1i1 268  i1id 269  i2id 270  ud1lem0c 271  ud2lem0c 272  ud4lem0c 274  ud5lem0c 275  wql2lem2 283  wql2lem3 284  wql2lem5 286  wql1 287  oaidlem1 288  womle2a 289  nomcon0 295  nomcon1 296  nomcon2 297  nomcon5 300  nom11 302  nom12 303  nom13 304  nom14 305  nom15 306  nom20 307  nom21 308  nom22 309  nom23 310  nom24 311  nom25 312  nom30 313  nom31 314  nom32 315  nom33 316  nom34 317  nom35 318  nom40 319  nom41 320  nom42 321  nom43 322  nom44 323  nom45 324  nom50 325  nom51 326  nom52 327  nom53 328  nom54 329  nom55 330  nom60 331  nom61 332  nom62 333  nom63 334  nom64 335  nom65 336  go1 337  i5lei1 341  i5lei3 343  2vwomr2 348  2vwomr1a 349  2vwomr2a 350  2vwomlem 351  wr5-2v 352  wlor 354  wran 355  wlan 356  wr2 357  wdf-le1 364  wdf-le2 365  wdf-c1 369  wdf-c2 370  wle0 376  wler 377  wcomcom 400  ska2 418  ska4 419  wom2 420  ka4ot 421  woml6 422  woml7 423  wed 427  r3b 428  lem3a.1 430  omln 432  omla 433  omlan 434  oml5 435  oml5a 436  oml3 438  comcom 439  comd 442  com3ii 443  comdr 452  com3i 453  df2c1 454  fh1 455  fh2 456  fh3 457  fh4 458  com2or 469  nbdi 472  oml4 473  oml6 474  gsth 475  gsth2 476  i0cmtrcom 481  i3bi 482  df2i3 484  dfi3b 485  dfi4b 486  i3n2 487  ni32 488  oi3ai3 489  i3lem1 490  i3lem3 492  i3lem4 493  lem4 497  i0i3 498  i3i0 499  ska14 500  i31 506  i3abs1 508  i3abs3 510  i3th1 529  i3th2 530  i3th3 531  i3th7 535  i3th8 536  i3con 537  i3orlem3 540  i3orlem5 542  i3orlem7 544  i3orlem8 545  ud1lem1 546  ud1lem2 547  ud1lem3 548  ud2lem1 549  ud2lem2 550  ud2lem3 551  ud3lem1a 552  ud3lem1b 553  ud3lem1c 554  ud3lem1d 555  ud3lem1 556  ud3lem2 557  ud3lem3b 559  ud3lem3c 560  ud3lem3d 561  ud3lem3 562  ud4lem1a 563  ud4lem1b 564  ud4lem1c 565  ud4lem1d 566  ud4lem1 567  ud4lem2 568  ud4lem3a 569  ud4lem3b 570  ud4lem3 571  ud5lem1a 572  ud5lem1b 573  ud5lem1c 574  ud5lem1 575  ud5lem2 576  ud5lem3a 577  ud5lem3b 578  ud5lem3c 579  ud5lem3 580  ud1 581  ud2 582  ud3 583  ud4 584  ud5 585  u1lemaa 586  u2lemaa 587  u3lemaa 588  u4lemaa 589  u5lemaa 590  u1lemana 591  u2lemana 592  u3lemana 593  u4lemana 594  u5lemana 595  u1lemab 596  u2lemab 597  u3lemab 598  u4lemab 599  u5lemab 600  u1lemanb 601  u2lemanb 602  u3lemanb 603  u4lemanb 604  u5lemanb 605  u1lemoa 606  u2lemoa 607  u3lemoa 608  u4lemoa 609  u5lemoa 610  u1lemona 611  u2lemona 612  u3lemona 613  u4lemona 614  u5lemona 615  u1lemob 616  u2lemob 617  u3lemob 618  u4lemob 619  u5lemob 620  u1lemonb 621  u2lemonb 622  u3lemonb 623  u4lemonb 624  u5lemonb 625  u1lemnaa 626  u2lemnaa 627  u3lemnaa 628  u4lemnaa 629  u5lemnaa 630  u1lemnana 631  u2lemnana 632  u3lemnana 633  u4lemnana 634  u5lemnana 635  u4lemnab 639  u5lemnab 640  u2lemnanb 642  u5lemnanb 645  u1lemnoa 646  u2lemnoa 647  u3lemnoa 648  u4lemnoa 649  u5lemnoa 650  u3lemnona 653  u4lemnob 659  u1lemnonb 661  u2lemnonb 662  u3lemnonb 663  u4lemnonb 664  u5lemnonb 665  u1lemc4 687  u2lemc4 688  u3lemc4 689  u4lemc4 690  u5lemc4 691  i1com 694  comi1 695  u1lemle1 696  u2lemle1 697  u3lemle1 698  u4lemle1 699  u5lemle1 700  u1lemle2 701  u2lemle2 702  u4lemle2 704  u5lemle2 705  u1lembi 706  u2lembi 707  u4lembi 710  u5lembi 711  u12lembi 712  oi3oa3 719  u1lem1 720  u2lem1 721  u3lem1 722  u4lem1 723  u5lem1 724  u3lem1n 727  u4lem1n 728  u5lem1n 729  u1lem2 730  u2lem2 731  u3lem2 732  u4lem2 733  u5lem2 734  u1lem3 735  u2lem3 736  u3lem3 737  u4lem3 738  u5lem3 739  u3lem3n 740  u4lem3n 741  u5lem3n 742  u1lem4 743  u3lem4 744  u4lem4 745  u5lem4 746  u1lem5 747  u2lem5 748  u3lem5 749  u4lem5 750  u5lem5 751  u4lem5n 752  u3lem6 753  u4lem6 754  u5lem6 755  u24lem 756  u12lem 757  u1lem7 758  u2lem7 759  u3lem7 760  u2lem7n 761  u1lem8 762  u1lem9a 763  u1lem11 766  u1lem12 767  u2lem8 768  u3lem8 769  u3lem9 770  u3lem10 771  u3lem11 772  u3lem11a 773  u3lem12 774  u3lem13a 775  u3lem13b 776  u3lem14a 777  u3lem14aa 778  u3lem14aa2 779  u3lem15 781  u3lemax4 782  u3lemax5 783  bi1o1a 784  biao 785  i2i1i1 786  i1abs 787  test 788  test2 789  3vth1 790  3vth3 792  3vth5 794  3vth6 795  3vth7 796  3vth8 797  3vth9 798  3vded11 800  3vded12 801  3vded13 802  3vded21 803  3vded22 804  3vded3 805  1oa 806  2oai1u 808  1oaiii 809  1oaii 810  2oalem1 811  2oath1 812  2oath1i1 813  1oath1i1u 814  oale 815  3vroa 817  mlalem 818  sa5 822  salem1 823  bi3 825  bi4 826  imp3 827  orbi 828  mlaconj4 830  mlaconj 831  i1orni1 833  negantlem1 834  negantlem2 835  negantlem3 836  negantlem4 837  negantlem9 845  negantlem10 847  neg3antlem1 850  neg3antlem2 851  elimconslem 853  elimcons2 855  comanblem1 856  comanblem2 857  comanb 858  mhlemlem1 860  mhlemlem2 861  mhlem 862  mhlem1 863  mhlem2 864  mh 865  marsdenlem1 866  marsdenlem2 867  marsdenlem3 868  marsdenlem4 869  mlaconjolem 871  mlaconjo 872  mhcor1 874  cancellem 877  e2ast2 880  e2astlem1 881  govar 882  go2n4 885  gomaex4 886  go2n6 887  gomaex3h10 897  gomaex3lem2 901  gomaex3lem3 902  gomaex3lem7 906  gomaex3 910  oas 911  oat 913  oatr 914  oau 915  oaur 916  oaidlem2 917  oaidlem2g 918  oa6v4v 919  oa4v3v 920  oal42 921  oa23 922  distoah4 929  distoa 930  oa3to4lem1 931  oa3to4lem2 932  oa3to4lem6 936  oa6todual 938  oa6fromdual 939  oa6to4h1 941  oa6to4h2 942  oa6to4h3 943  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  oa8todual 957  oa4to4u 959  oa4uto4g 961  oa4gto4u 962  oa3-2lema 964  oa3-2lemb 965  oa3-6lem 966  oa3-3lem 967  oa3-1lem 968  oa3-5lem 970  oa3-u2lem 972  oa3-6to3 973  oa3-2to4 974  oa3-2to2s 976  oa3-u1 977  oa3-u2 978  oa3-1to5 979  d3oa 981  d4oa 982  oaliii 987  oalii 988  oaliv 989  oalem1 991  oalem2 992  oadist2a 993  oacom 997  oagen1 1000  oagen1b 1001  mloa 1004  oadist 1005  oadistb 1006  oadistc0 1007  oadistc 1008  oadistd 1009  3oa2 1010  axoa4a 1022  4oaiii 1025  4oath1 1026  4oagen1 1027  4oagen1b 1028  4oadist 1029  lem3.3.2 1031  lem3.3.4 1038  lem3.3.6 1041  lem3.3.7i2e2 1049  lem3.3.7i3e1 1051  lem3.3.7i3e2 1052  lem3.3.7i4e2 1055  lem3.4.1 1060  lem3.4.4 1062  lem3.4.6 1064  lem4.6.6i1j3 1077  lem4.6.6i2j4 1080  lem4.6.6i3j0 1081  lem4.6.6i3j1 1082  lem4.6.6i4j2 1084  com3iia 1085  lem4.6.7 1086  wdcom 1088  wdwom 1089  wdid0id5 1094  wdid0id1 1095  wdid0id2 1096  wdid0id3 1097  wdid0id4 1098

Copyright terms: Public domain