Axiom ax-r2 35

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 58  tt 59  3tr1 60  3tr 62  con2 64  con3 65  2or 67  2an 72  anor1 80  anor2 81  dfb 86  dfnb 87  2bi 91  dff2 92  dff 93  or0 94  or0r 95  or1 96  or1r 97  an1 98  an1r 99  an0 100  an0r 101  oridm 102  anidm 103  orordi 104  orordir 105  anandi 106  anandir 107  1b 109  bi1 110  a5b 112  a5c 113  conb 114  leoa 115  leao 116  mi 117  di 118  omlem1 119  letr 129  bltr 130  lbtr 131  bile 134  lebi 137  le0 139  ler 141  lel 143  leror 144  leran 145  lea 152  comm0 170  comm1 171  lecom 172  cbtr 174  comcom2 175  cmtrcom 182  wr1 189  wr3 190  wr4 191  wwbmp 197  wcon1 199  wcon2 200  wcon3 201  wlem3.1 202  wwoml3 205  wwcomd 206  wwcom3ii 207  wwfh1 208  wwfh2 209  wwfh3 210  wwfh4 211  ka4lemo 220  ka4lem 221  sklem 222  ska8 228  skr0 234  wlem1 235  lei3 238  mccune2 239  mccune3 240  i3n1 241  ni31 242  i3id 243  2i3 246  ud1lem0ab 249  i1i2 258  i1i2con1 260  i1i2con2 261  i3i4 262  i4i3 263  i5con 264  0i1 265  1i1 266  i1id 267  i2id 268  ud1lem0c 269  ud2lem0c 270  ud4lem0c 272  ud5lem0c 273  wql2lem2 281  wql2lem3 282  wql2lem5 284  wql1 285  oaidlem1 286  womle2a 287  nomcon0 293  nomcon1 294  nomcon2 295  nomcon5 298  nom11 300  nom12 301  nom13 302  nom14 303  nom15 304  nom20 305  nom21 306  nom22 307  nom23 308  nom24 309  nom25 310  nom30 311  nom31 312  nom32 313  nom33 314  nom34 315  nom35 316  nom40 317  nom41 318  nom42 319  nom43 320  nom44 321  nom45 322  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  nom55 328  nom60 329  nom61 330  nom62 331  nom63 332  nom64 333  nom65 334  go1 335  i5lei1 339  i5lei3 341  2vwomr2 344  2vwomr1a 345  2vwomr2a 346  2vwomlem 347  wr5-2v 348  wlor 350  wran 351  wlan 352  wr2 353  wdf-le1 360  wdf-le2 361  wdf-c1 365  wdf-c2 366  wle0 372  wler 373  wcomcom 396  wr5 413  ska2 414  ska4 415  wom2 416  ka4ot 417  woml6 418  woml7 419  wed 423  r3b 424  lem3.1 425  lem3a.1 426  omln 428  omla 429  omlan 430  oml5 431  oml5a 432  oml3 434  comcom 435  comd 438  com3ii 439  comdr 448  com3i 449  df2c1 450  fh1 451  fh2 452  fh3 453  fh4 454  com2or 465  nbdi 468  oml4 469  oml6 470  gsth 471  gsth2 472  i0cmtrcom 477  i3bi 478  df2i3 480  dfi3b 481  dfi4b 482  i3n2 483  ni32 484  oi3ai3 485  i3lem1 486  i3lem3 488  i3lem4 489  lem4 493  i0i3 494  i3i0 495  ska14 496  i31 502  i3abs1 504  i3abs3 506  i3th1 525  i3th2 526  i3th3 527  i3th7 531  i3th8 532  i3con 533  i3orlem3 536  i3orlem5 538  i3orlem7 540  i3orlem8 541  ud1lem1 542  ud1lem2 543  ud1lem3 544  ud2lem1 545  ud2lem2 546  ud2lem3 547  ud3lem1a 548  ud3lem1b 549  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem2 553  ud3lem3b 555  ud3lem3c 556  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  ud4lem3a 565  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1c 570  ud5lem1 571  ud5lem2 572  ud5lem3a 573  ud5lem3b 574  ud5lem3c 575  ud5lem3 576  ud1 577  ud2 578  ud3 579  ud4 580  ud5 581  u1lemaa 582  u2lemaa 583  u3lemaa 584  u4lemaa 585  u5lemaa 586  u1lemana 587  u2lemana 588  u3lemana 589  u4lemana 590  u5lemana 591  u1lemab 592  u2lemab 593  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u1lemoa 602  u2lemoa 603  u3lemoa 604  u4lemoa 605  u5lemoa 606  u1lemona 607  u2lemona 608  u3lemona 609  u4lemona 610  u5lemona 611  u1lemob 612  u2lemob 613  u3lemob 614  u4lemob 615  u5lemob 616  u1lemonb 617  u2lemonb 618  u3lemonb 619  u4lemonb 620  u5lemonb 621  u1lemnaa 622  u2lemnaa 623  u3lemnaa 624  u4lemnaa 625  u5lemnaa 626  u1lemnana 627  u2lemnana 628  u3lemnana 629  u4lemnana 630  u5lemnana 631  u4lemnab 635  u5lemnab 636  u2lemnanb 638  u5lemnanb 641  u1lemnoa 642  u2lemnoa 643  u3lemnoa 644  u4lemnoa 645  u5lemnoa 646  u3lemnona 649  u4lemnob 655  u1lemnonb 657  u2lemnonb 658  u3lemnonb 659  u4lemnonb 660  u5lemnonb 661  u1lemc4 683  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  i1com 690  comi1 691  u1lemle1 692  u2lemle1 693  u3lemle1 694  u4lemle1 695  u5lemle1 696  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u1lembi 702  u2lembi 703  u4lembi 706  u5lembi 707  u12lembi 708  oi3oa3 715  u1lem1 716  u2lem1 717  u3lem1 718  u4lem1 719  u5lem1 720  u3lem1n 723  u4lem1n 724  u5lem1n 725  u1lem2 726  u2lem2 727  u3lem2 728  u4lem2 729  u5lem2 730  u1lem3 731  u2lem3 732  u3lem3 733  u4lem3 734  u5lem3 735  u3lem3n 736  u4lem3n 737  u5lem3n 738  u1lem4 739  u3lem4 740  u4lem4 741  u5lem4 742  u1lem5 743  u2lem5 744  u3lem5 745  u4lem5 746  u5lem5 747  u4lem5n 748  u3lem6 749  u4lem6 750  u5lem6 751  u24lem 752  u12lem 753  u1lem7 754  u2lem7 755  u3lem7 756  u2lem7n 757  u1lem8 758  u1lem9a 759  u1lem11 762  u1lem12 763  u2lem8 764  u3lem8 765  u3lem9 766  u3lem10 767  u3lem11 768  u3lem11a 769  u3lem12 770  u3lem13a 771  u3lem13b 772  u3lem14a 773  u3lem14aa 774  u3lem14aa2 775  u3lem15 777  u3lemax4 778  u3lemax5 779  bi1o1a 780  biao 781  i2i1i1 782  i1abs 783  test 784  test2 785  3vth1 786  3vth3 788  3vth5 790  3vth6 791  3vth7 792  3vth8 793  3vth9 794  3vded11 796  3vded12 797  3vded13 798  3vded21 799  3vded22 800  3vded3 801  1oa 802  2oai1u 804  1oaiii 805  1oaii 806  2oalem1 807  2oath1 808  2oath1i1 809  1oath1i1u 810  oale 811  3vroa 813  mlalem 814  sa5 818  salem1 819  bi3 821  bi4 822  imp3 823  orbi 824  mlaconj4 826  mlaconj 827  i1orni1 829  negantlem1 830  negantlem2 831  negantlem3 832  negantlem4 833  negantlem9 841  negantlem10 843  neg3antlem1 846  neg3antlem2 847  elimconslem 849  elimcons2 851  comanblem1 852  comanblem2 853  comanb 854  mhlemlem1 856  mhlemlem2 857  mhlem 858  mhlem1 859  mhlem2 860  mh 861  marsdenlem1 862  marsdenlem2 863  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mlaconjo 868  mhcor1 870  cancellem 873  govar 876  go2n4 879  gomaex4 880  go2n6 881  gomaex3h10 891  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem7 900  gomaex3 904  oas 905  oat 907  oatr 908  oau 909  oaur 910  oaidlem2 911  oaidlem2g 912  oa6v4v 913  oa4v3v 914  oal42 915  oa23 916  distoah4 923  distoa 924  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem6 930  oa6todual 932  oa6fromdual 933  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa8todual 951  oa4to4u 953  oa4uto4g 955  oa4gto4u 956  oa3-2lema 958  oa3-2lemb 959  oa3-6lem 960  oa3-3lem 961  oa3-1lem 962  oa3-5lem 964  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-2to2s 970  oa3-u1 971  oa3-u2 972  oa3-1to5 973  d3oa 975  d4oa 976  oaliii 981  oalii 982  oaliv 983  oalem1 985  oalem2 986  oadist2a 987  oacom 991  oagen1 994  oagen1b 995  mloa 998  oadist 999  oadistb 1000  oadistc0 1001  oadistc 1002  oadistd 1003  3oa2 1004  axoa4a 1016  4oaiii 1019  4oath1 1020  4oagen1 1021  4oagen1b 1022  4oadist 1023

metamath.org