Axiom ax-r1 35

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 59  tt 60  3tr1 61  3tr2 62  con2 65  anor1 82  anor2 83  anor3 84  oran1 85  oran2 86  oran3 87  dfb 88  dfnb 89  dff 95  or1 98  an1 100  oridm 104  orordi 106  orordir 107  anandi 108  anandir 109  1b 111  1bi 113  leoa 117  leao 118  di 120  omlem1 121  omlem2 122  letr 131  lbtr 133  le3tr1 134  le3tr2 135  qlhoml1b 138  lebi 139  ler 143  leror 146  leran 147  ler2or 166  ler2an 167  ledi 168  ledio 170  comm0 172  comm1 173  lecom 174  wr3 192  wr4 193  wwbmp 199  wcon2 202  wcon3 203  wlem3.1 204  wwoml2 206  wwoml3 207  wwcomd 208  wwcom3ii 209  wwfh1 210  wwfh2 211  wwfh4 213  ka4lemo 222  ka4lem 223  sklem 224  ska6 228  ska8 230  skr0 236  wlem1 237  mccune2 241  mccune3 242  i3n1 243  ni31 244  i3id 245  i1i2con1 262  i1i2con2 263  i4i3 265  1i1 268  i2id 270  ud1lem0c 271  ud2lem0c 272  ud4lem0c 274  ud5lem0c 275  wql1lem 281  wql2lem2 283  wql2lem3 284  wql2lem4 285  wql1 287  womle2b 290  womle3b 291  womle 292  nom11 302  nom12 303  nom13 304  nom14 305  nom15 306  nom20 307  nom21 308  nom22 309  nom23 310  nom24 311  nom25 312  nom31 314  nom32 315  nom40 319  nom41 320  nom42 321  nom43 322  nom44 323  nom45 324  nom50 325  nom51 326  nom52 327  nom53 328  nom54 329  nom55 330  nom61 332  nom62 333  go1 337  i2or 338  i1or 339  2vwomr2 348  2vwomr1a 349  2vwomr2a 350  2vwomlem 351  wr5-2v 352  wom3 353  wdf-le2 365  wdf-c2 370  wler 377  wcom2an 414  wlem14 416  ska2 418  ska4 419  wom2 420  woml6 422  woml7 423  ortha 424  lem3.1 429  lem3a.1 430  omla 433  oml3 438  comcom 439  comd 442  com3ii 443  df2c1 454  fh1 455  fh2 456  fh3 457  fh4 458  com2or 469  com2an 470  combi 471  oml4 473  oml6 474  gsth 475  gsth2 476  gstho 477  cmtr1com 479  comcmtr1 480  i0cmtrcom 481  i3bi 482  i3or 483  dfi3b 485  dfi4b 486  i3n2 487  ni32 488  oi3ai3 489  i3lem1 490  i3lem2 491  i3lem3 492  i3lem4 493  comi31 494  com2i3 495  lem4 497  i3i0 499  ska14 500  bii3 502  i3abs3 510  i33tr1 515  i33tr2 516  i3th1 529  i3th4 532  i3th7 535  i3th8 536  i3con 537  i3orlem1 538  i3orlem3 540  i3orlem4 541  i3orlem5 542  i3orlem6 543  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  ud3lem3d 561  ud3lem3 562  ud4lem1a 563  ud4lem1b 564  ud4lem1c 565  ud4lem1d 566  ud4lem1 567  ud4lem2 568  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  u3lemana 593  u4lemana 594  u5lemana 595  u3lemab 598  u4lemab 599  u5lemab 600  u1lemanb 601  u2lemanb 602  u3lemanb 603  u4lemanb 604  u5lemanb 605  u1lemoa 606  u2lemoa 607  u4lemoa 609  u5lemoa 610  u4lemona 614  u3lemob 618  u4lemob 619  u1lemonb 621  u2lemonb 622  u3lemonb 623  u1lemnaa 626  u2lemnaa 627  u3lemnaa 628  u4lemnaa 629  u5lemnaa 630  u1lemnana 631  u2lemnana 632  u4lemnana 634  u1lemnab 636  u2lemnab 637  u3lemnab 638  u1lemnoa 646  u2lemnonb 662  u1lemc1 666  u2lemc1 667  u4lemc1 669  u5lemc1 670  u5lemc1b 671  u1lemc2 672  u2lemc2 673  u4lemc2 675  u5lemc2 676  u1lemc4 687  u2lemc4 688  u3lemc4 689  u4lemc4 690  u5lemc4 691  comi12 693  u1lemle2 701  u2lemle2 702  u4lemle2 704  u5lemle2 705  u1lembi 706  u2lembi 707  i2bi 708  u4lembi 710  u5lembi 711  u12lembi 712  u1lemn1b 716  u1lem3var1 717  u2lem1 721  u3lem1n 727  u4lem1n 728  u5lem1n 729  u1lem2 730  u2lem2 731  u1lem3 735  u2lem3 736  u1lem4 743  u4lem4 745  u5lem4 746  u1lem5 747  u4lem5 750  u5lem5 751  u3lem6 753  u4lem6 754  u5lem6 755  u24lem 756  u1lem7 758  u2lem7 759  u3lem7 760  u1lem8 762  u1lem9a 763  u1lem9b 764  u1lem11 766  u2lem8 768  u3lem8 769  u3lem9 770  u3lem10 771  u3lem11 772  u3lem12 774  u3lem13a 775  u3lem13b 776  u3lem14a 777  u3lem14aa2 779  u3lem14mp 780  u3lem15 781  u3lemax4 782  u3lemax5 783  bi1o1a 784  biao 785  i2i1i1 786  i1abs 787  test 788  test2 789  3vth1 790  3vth5 794  3vth6 795  3vth7 796  3vth8 797  3vth9 798  3vcom 799  3vded11 800  3vded12 801  3vded13 802  3vded21 803  3vded22 804  3vded3 805  1oa 806  1oai1 807  2oai1u 808  1oaiii 809  2oalem1 811  2oath1 812  2oath1i1 813  1oath1i1u 814  oale 815  3vroa 817  mlalem 818  sa5 822  salem1 823  sadm3 824  bi3 825  bi4 826  orbi 828  mlaconj4 830  i1orni1 833  negantlem1 834  negantlem2 835  negantlem3 836  negantlem4 837  negant 838  negantlem9 845  negant3 846  negantlem10 847  negant4 848  neg3antlem1 850  neg3antlem2 851  neg3ant1 852  elimconslem 853  elimcons 854  elimcons2 855  comanblem1 856  comanblem2 857  comanbn 859  mhlem 862  mhlem1 863  mh 865  marsdenlem2 867  marsdenlem3 868  marsdenlem4 869  mlaconjolem 871  mlaconjo 872  mhcor1 874  oago3.29 875  oago3.21x 876  cancellem 877  cancel 878  e2ast2 880  govar 882  govar2 883  go2n4 885  go2n6 887  gomaex3h7 894  gomaex3h10 897  gomaex3lem1 900  gomaex3lem2 901  gomaex3lem3 902  gomaex3lem4 903  gomaex3lem7 906  gomaex3lem9 908  gomaex3 910  oas 911  oat 913  oatr 914  oau 915  oaidlem2 917  oaidlem2g 918  oa23 922  distoah2 927  distoah3 928  distoa 930  oa3to4lem1 931  oa3to4lem2 932  oa6to4h1 941  oa6to4h2 942  oa6to4h3 943  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  oa4btoc 952  oa4to4u 959  oa4gto4u 962  oa3-6lem 966  oa3-3lem 967  oa3-4lem 969  oa3-u1lem 971  oa3-u2lem 972  oa3-6to3 973  oa3-2to4 974  oa3-2to2s 976  oa3-u1 977  oa3-u2 978  d3oa 981  d4oa 982  oal2 985  oaliii 987  oaliv 989  oath1 990  oalem1 991  oadist2a 993  oadist2b 994  oagen1b 1001  mloa 1004  oadist 1005  oadistb 1006  oadistc0 1007  oadistc 1008  oadistd 1009  axoa4a 1022  axoa4d 1023  4oath1 1026  4oagen1 1027  4oagen1b 1028  4oadist 1029  lem3.3.2 1031  lem3.3.4 1038  lem3.3.5 1040  lem3.3.6 1041  lem3.3.7i0e1 1042  lem3.3.7i1e1 1045  lem3.3.7i1e2 1046  lem3.3.7i2e1 1048  lem3.3.7i2e2 1049  lem3.3.7i3e1 1051  lem3.3.7i3e2 1052  lem3.3.7i4e1 1054  lem3.3.7i4e2 1055  lem3.3.7i5e1 1057  lem3.3.7i5e2 1058  lem3.4.3 1061  lem3.4.4 1062  lem3.4.6 1064  lem4.6.2e1 1065  lem4.6.5 1070  lem4.6.6i1j3 1077  lem4.6.6i2j4 1080  lem4.6.6i3j0 1081  lem4.6.6i3j1 1082  lem4.6.6i4j2 1084  lem4.6.7 1086  wdcom 1088  wdwom 1089  wdid0id5 1094  wdid0id1 1095  wdid0id2 1096  wdid0id3 1097  wdid0id4 1098

Copyright terms: Public domain