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  cm 61  3tr1 63  3tr2 64  con2 67  anor1 88  anor2 89  anor3 90  oran1 91  oran2 92  oran3 93  dfb 94  dfnb 95  dff 101  or1 104  an1 106  oridm 110  orordi 112  orordir 113  anandi 114  anandir 115  1b 117  1bi 119  leoa 123  leao 124  di 126  omlem1 127  omlem2 128  letr 137  lbtr 139  le3tr1 140  le3tr2 141  qlhoml1b 144  lebi 145  ler 149  leror 152  leran 153  ler2or 172  ler2an 173  ledi 174  ledio 176  comm0 178  comm1 179  lecom 180  wr3 198  wr4 199  wwbmp 205  wcon2 208  wcon3 209  wlem3.1 210  wwoml2 212  wwoml3 213  wwcomd 214  wwcom3ii 215  wwfh1 216  wwfh2 217  wwfh4 219  ka4lemo 228  ka4lem 229  sklem 230  ska6 234  ska8 236  skr0 242  wlem1 243  mccune2 247  mccune3 248  i3n1 249  ni31 250  i3id 251  i1i2con1 268  i1i2con2 269  i4i3 271  1i1 274  i2id 276  ud1lem0c 277  ud2lem0c 278  ud4lem0c 280  ud5lem0c 281  wql1lem 287  wql2lem2 289  wql2lem3 290  wql2lem4 291  wql1 293  womle2b 296  womle3b 297  womle 298  nom11 308  nom12 309  nom13 310  nom14 311  nom15 312  nom20 313  nom21 314  nom22 315  nom23 316  nom24 317  nom25 318  nom31 320  nom32 321  nom40 325  nom41 326  nom42 327  nom43 328  nom44 329  nom45 330  nom50 331  nom51 332  nom52 333  nom53 334  nom54 335  nom55 336  nom61 338  nom62 339  go1 343  i2or 344  i1or 345  k1-2 357  k1-3 358  2vwomr2 362  2vwomr1a 363  2vwomr2a 364  2vwomlem 365  wr5-2v 366  wom3 367  wdf-le2 379  wdf-c2 384  wler 391  wcom2an 428  wlem14 430  ska2 432  ska4 433  wom2 434  woml6 436  woml7 437  ortha 438  lem3.1 443  lem3a.1 444  omla 447  oml3 452  comcom 453  comd 456  com3ii 457  df2c1 468  fh1 469  fh2 470  fh3 471  fh4 472  com2or 483  com2an 484  combi 485  oml4 487  oml6 488  gsth 489  gsth2 490  gstho 491  cmtr1com 493  comcmtr1 494  i0cmtrcom 495  i3bi 496  i3or 497  dfi3b 499  dfi4b 500  i3n2 501  ni32 502  oi3ai3 503  i3lem1 504  i3lem2 505  i3lem3 506  i3lem4 507  comi31 508  com2i3 509  lem4 511  i3i0 513  ska14 514  bii3 516  i3abs3 524  i33tr1 529  i33tr2 530  i3th1 543  i3th4 546  i3th7 549  i3th8 550  i3con 551  i3orlem1 552  i3orlem3 554  i3orlem4 555  i3orlem5 556  i3orlem6 557  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  ud3lem3d 575  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1d 580  ud4lem1 581  ud4lem2 582  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  u3lemana 607  u4lemana 608  u5lemana 609  u3lemab 612  u4lemab 613  u5lemab 614  u1lemanb 615  u2lemanb 616  u3lemanb 617  u4lemanb 618  u5lemanb 619  u1lemoa 620  u2lemoa 621  u4lemoa 623  u5lemoa 624  u4lemona 628  u3lemob 632  u4lemob 633  u1lemonb 635  u2lemonb 636  u3lemonb 637  u1lemnaa 640  u2lemnaa 641  u3lemnaa 642  u4lemnaa 643  u5lemnaa 644  u1lemnana 645  u2lemnana 646  u4lemnana 648  u1lemnab 650  u2lemnab 651  u3lemnab 652  u1lemnoa 660  u2lemnonb 676  u1lemc1 680  u2lemc1 681  u4lemc1 683  u5lemc1 684  u5lemc1b 685  u1lemc2 686  u2lemc2 687  u4lemc2 689  u5lemc2 690  u1lemc4 701  u2lemc4 702  u3lemc4 703  u4lemc4 704  u5lemc4 705  comi12 707  u1lemle2 715  u2lemle2 716  u4lemle2 718  u5lemle2 719  u1lembi 720  u2lembi 721  i2bi 722  u4lembi 724  u5lembi 725  u12lembi 726  u1lemn1b 730  u1lem3var1 731  u2lem1 735  u3lem1n 741  u4lem1n 742  u5lem1n 743  u1lem2 744  u2lem2 745  u1lem3 749  u2lem3 750  u1lem4 757  u4lem4 759  u5lem4 760  u1lem5 761  u4lem5 764  u5lem5 765  u3lem6 767  u4lem6 768  u5lem6 769  u24lem 770  u1lem7 772  u2lem7 773  u3lem7 774  u1lem8 776  u1lem9a 777  u1lem9b 778  u1lem11 780  u2lem8 782  u3lem8 783  u3lem9 784  u3lem10 785  u3lem11 786  u3lem12 788  u3lem13a 789  u3lem13b 790  u3lem14a 791  u3lem14aa2 793  u3lem14mp 794  u3lem15 795  u3lemax4 796  u3lemax5 797  bi1o1a 798  biao 799  i2i1i1 800  i1abs 801  test 802  test2 803  3vth1 804  3vth5 808  3vth6 809  3vth7 810  3vth8 811  3vth9 812  3vcom 813  3vded11 814  3vded12 815  3vded13 816  3vded21 817  3vded22 818  3vded3 819  1oa 820  1oai1 821  2oai1u 822  1oaiii 823  2oalem1 825  2oath1 826  2oath1i1 827  1oath1i1u 828  oale 829  3vroa 831  mlalem 832  sa5 836  salem1 837  sadm3 838  bi3 839  bi4 840  orbi 842  mlaconj4 844  i1orni1 847  negantlem1 848  negantlem2 849  negantlem3 850  negantlem4 851  negant 852  negantlem9 859  negant3 860  negantlem10 861  negant4 862  neg3antlem1 864  neg3antlem2 865  neg3ant1 866  elimconslem 867  elimcons 868  elimcons2 869  comanblem1 870  comanblem2 871  comanbn 873  mhlem 876  mhlem1 877  mh 879  marsdenlem2 881  marsdenlem3 882  marsdenlem4 883  mlaconjolem 885  mlaconjo 886  mhcor1 888  oago3.29 889  oago3.21x 890  cancellem 891  cancel 892  e2ast2 894  govar 896  govar2 897  go2n4 899  go2n6 901  gomaex3h7 908  gomaex3h10 911  gomaex3lem1 914  gomaex3lem2 915  gomaex3lem3 916  gomaex3lem4 917  gomaex3lem7 920  gomaex3lem9 922  gomaex3 924  oas 925  oat 927  oatr 928  oau 929  oaidlem2 931  oaidlem2g 932  oa23 936  distoah2 941  distoah3 942  distoa 944  oa3to4lem1 945  oa3to4lem2 946  oa6to4h1 955  oa6to4h2 956  oa6to4h3 957  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa4btoc 966  oa4to4u 973  oa4gto4u 976  oa3-6lem 980  oa3-3lem 981  oa3-4lem 983  oa3-u1lem 985  oa3-u2lem 986  oa3-6to3 987  oa3-2to4 988  oa3-2to2s 990  oa3-u1 991  oa3-u2 992  d3oa 995  d4oa 996  oal2 999  oaliii 1001  oaliv 1003  oath1 1004  oalem1 1005  oadist2a 1007  oadist2b 1008  oagen1b 1015  mloa 1018  oadist 1019  oadistb 1020  oadistc0 1021  oadistc 1022  oadistd 1023  axoa4a 1036  axoa4d 1037  4oath1 1040  4oagen1 1041  4oagen1b 1042  4oadist 1043  lem3.3.2 1045  lem3.3.4 1052  lem3.3.5 1054  lem3.3.6 1055  lem3.3.7i0e1 1056  lem3.3.7i1e1 1059  lem3.3.7i1e2 1060  lem3.3.7i2e1 1062  lem3.3.7i2e2 1063  lem3.3.7i3e1 1065  lem3.3.7i3e2 1066  lem3.3.7i4e1 1068  lem3.3.7i4e2 1069  lem3.3.7i5e1 1071  lem3.3.7i5e2 1072  lem3.4.3 1075  lem3.4.4 1076  lem3.4.6 1078  lem4.6.2e1 1079  lem4.6.5 1084  lem4.6.6i1j3 1091  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098  lem4.6.7 1100  wdcom 1102  wdwom 1103  wdid0id5 1108  wdid0id1 1109  wdid0id2 1110  wdid0id3 1111  wdid0id4 1112

Copyright terms: Public domain