Axiom ax-r1 34

Description: Inference rule for ortholattices.

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 58  tt 59  3tr1 60  3tr2 61  con2 64  anor1 80  anor2 81  anor3 82  oran1 83  oran2 84  oran3 85  dfb 86  dfnb 87  dff 93  or1 96  an1 98  oridm 102  orordi 104  orordir 105  anandi 106  anandir 107  1b 109  1bi 111  leoa 115  leao 116  di 118  omlem1 119  omlem2 120  letr 129  lbtr 131  le3tr1 132  le3tr2 133  qlhoml1b 136  lebi 137  ler 141  leror 144  leran 145  ler2or 164  ler2an 165  ledi 166  ledio 168  comm0 170  comm1 171  lecom 172  wr3 190  wr4 191  wwbmp 197  wcon2 200  wcon3 201  wlem3.1 202  wwoml2 204  wwoml3 205  wwcomd 206  wwcom3ii 207  wwfh1 208  wwfh2 209  wwfh4 211  ka4lemo 220  ka4lem 221  sklem 222  ska6 226  ska8 228  skr0 234  wlem1 235  mccune2 239  mccune3 240  i3n1 241  ni31 242  i3id 243  i1i2con1 260  i1i2con2 261  i4i3 263  1i1 266  i2id 268  ud1lem0c 269  ud2lem0c 270  ud4lem0c 272  ud5lem0c 273  wql1lem 279  wql2lem2 281  wql2lem3 282  wql2lem4 283  wql1 285  womle2b 288  womle3b 289  womle 290  nom11 300  nom12 301  nom13 302  nom14 303  nom15 304  nom20 305  nom21 306  nom22 307  nom23 308  nom24 309  nom25 310  nom31 312  nom32 313  nom40 317  nom41 318  nom42 319  nom43 320  nom44 321  nom45 322  nom50 323  nom51 324  nom52 325  nom53 326  nom54 327  nom55 328  nom61 330  nom62 331  go1 335  i2or 336  i1or 337  2vwomr2 344  2vwomr1a 345  2vwomr2a 346  2vwomlem 347  wr5-2v 348  wom3 349  wdf-le2 361  wdf-c2 366  wler 373  wcom2an 410  wlem14 412  wr5 413  ska2 414  ska4 415  wom2 416  woml6 418  woml7 419  ortha 420  lem3.1 425  lem3a.1 426  omla 429  oml3 434  comcom 435  comd 438  com3ii 439  df2c1 450  fh1 451  fh2 452  fh3 453  fh4 454  com2or 465  com2an 466  combi 467  oml4 469  oml6 470  gsth 471  gsth2 472  gstho 473  cmtr1com 475  comcmtr1 476  i0cmtrcom 477  i3bi 478  i3or 479  dfi3b 481  dfi4b 482  i3n2 483  ni32 484  oi3ai3 485  i3lem1 486  i3lem2 487  i3lem3 488  i3lem4 489  comi31 490  com2i3 491  lem4 493  i3i0 495  ska14 496  bii3 498  i3abs3 506  i33tr1 511  i33tr2 512  i3th1 525  i3th4 528  i3th7 531  i3th8 532  i3con 533  i3orlem1 534  i3orlem3 536  i3orlem4 537  i3orlem5 538  i3orlem6 539  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  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud4lem2 564  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  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u1lemanb 597  u2lemanb 598  u3lemanb 599  u4lemanb 600  u5lemanb 601  u1lemoa 602  u2lemoa 603  u4lemoa 605  u5lemoa 606  u4lemona 610  u3lemob 614  u4lemob 615  u1lemonb 617  u2lemonb 618  u3lemonb 619  u1lemnaa 622  u2lemnaa 623  u3lemnaa 624  u4lemnaa 625  u5lemnaa 626  u1lemnana 627  u2lemnana 628  u4lemnana 630  u1lemnab 632  u2lemnab 633  u3lemnab 634  u1lemnoa 642  u2lemnonb 658  u1lemc1 662  u2lemc1 663  u4lemc1 665  u5lemc1 666  u5lemc1b 667  u1lemc2 668  u2lemc2 669  u4lemc2 671  u5lemc2 672  u1lemc4 683  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  comi12 689  u1lemle2 697  u2lemle2 698  u4lemle2 700  u5lemle2 701  u1lembi 702  u2lembi 703  i2bi 704  u4lembi 706  u5lembi 707  u12lembi 708  u1lemn1b 712  u1lem3var1 713  u2lem1 717  u3lem1n 723  u4lem1n 724  u5lem1n 725  u1lem2 726  u2lem2 727  u1lem3 731  u2lem3 732  u1lem4 739  u4lem4 741  u5lem4 742  u1lem5 743  u4lem5 746  u5lem5 747  u3lem6 749  u4lem6 750  u5lem6 751  u24lem 752  u1lem7 754  u2lem7 755  u3lem7 756  u1lem8 758  u1lem9a 759  u1lem9b 760  u1lem11 762  u2lem8 764  u3lem8 765  u3lem9 766  u3lem10 767  u3lem11 768  u3lem12 770  u3lem13a 771  u3lem13b 772  u3lem14a 773  u3lem14aa2 775  u3lem14mp 776  u3lem15 777  u3lemax4 778  u3lemax5 779  bi1o1a 780  biao 781  i2i1i1 782  i1abs 783  test 784  test2 785  3vth1 786  3vth5 790  3vth6 791  3vth7 792  3vth8 793  3vth9 794  3vcom 795  3vded11 796  3vded12 797  3vded13 798  3vded21 799  3vded22 800  3vded3 801  1oa 802  1oai1 803  2oai1u 804  1oaiii 805  2oalem1 807  2oath1 808  2oath1i1 809  1oath1i1u 810  oale 811  3vroa 813  mlalem 814  sa5 818  salem1 819  sadm3 820  bi3 821  bi4 822  orbi 824  mlaconj4 826  i1orni1 829  negantlem1 830  negantlem2 831  negantlem3 832  negantlem4 833  negant 834  negantlem9 841  negant3 842  negantlem10 843  negant4 844  neg3antlem1 846  neg3antlem2 847  neg3ant1 848  elimconslem 849  elimcons 850  elimcons2 851  comanblem1 852  comanblem2 853  comanbn 855  mhlem 858  mhlem1 859  mh 861  marsdenlem2 863  marsdenlem3 864  marsdenlem4 865  mlaconjolem 867  mlaconjo 868  mhcor1 870  oago3.29 871  oago3.21x 872  cancellem 873  cancel 874  govar 876  govar2 877  go2n4 879  go2n6 881  gomaex3h7 888  gomaex3h10 891  gomaex3lem1 894  gomaex3lem2 895  gomaex3lem3 896  gomaex3lem4 897  gomaex3lem7 900  gomaex3lem9 902  gomaex3 904  oas 905  oat 907  oatr 908  oau 909  oaidlem2 911  oaidlem2g 912  oa23 916  distoah2 921  distoah3 922  distoa 924  oa3to4lem1 925  oa3to4lem2 926  oa6to4h1 935  oa6to4h2 936  oa6to4h3 937  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4btoc 946  oa4to4u 953  oa4gto4u 956  oa3-6lem 960  oa3-3lem 961  oa3-4lem 963  oa3-u1lem 965  oa3-u2lem 966  oa3-6to3 967  oa3-2to4 968  oa3-2to2s 970  oa3-u1 971  oa3-u2 972  d3oa 975  d4oa 976  oal2 979  oaliii 981  oaliv 983  oath1 984  oalem1 985  oadist2a 987  oadist2b 988  oagen1b 995  mloa 998  oadist 999  oadistb 1000  oadistc0 1001  oadistc 1002  oadistd 1003  axoa4a 1016  axoa4d 1017  4oath1 1020  4oagen1 1021  4oagen1b 1022  4oadist 1023

metamath.org