NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  bitri Structured version   Unicode version

Theorem bitri 240
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypotheses
Ref Expression
bitri.1
bitri.2
Assertion
Ref Expression
bitri

Proof of Theorem bitri
StepHypRef Expression
1 bitri.1 . . . 4
21biimpi 186 . . 3
3 bitri.2 . . 3
42, 3sylib 188 . 2
53biimpri 197 . . 3
65, 1sylibr 203 . 2
74, 6impbii 180 1
Colors of variables: wff set class
Syntax hints:   wb 176
This theorem is referenced by:  bitr2i  241  bitr3i  242  bitr4i  243  bitrd  244  3bitri  262  3bitr2i  264  3bitr3i  266  3bitr4i  268  xchbinx  301  bibi12i  306  imbi12i  316  mt2bi  328  iman  413  orbi12i  507  or42  515  pm4.71r  612  biadan2  623  anbi2ci  677  anbi12i  678  anbi12ci  679  pm5.3  692  pm5.53  771  an42  798  orddi  839  anddi  840  rbaib  873  rbaibr  874  pm4.43  893  biluk  899  pm5.75  903  dn1  932  3orass  937  3anass  938  3ancomb  943  3anan32  946  3anan12  947  3anor  948  an6  1261  xor2  1310  falbitru  1352  falnantru  1356  truxortru  1358  truxorfal  1359  falxorfal  1361  exp3acom23g  1371  hadass  1386  hadbi  1387  hadrot  1390  cador  1391  cadan  1392  cadnot  1394  cadcomb  1396  cadrot  1397  cad1  1398  had1  1402  alex  1572  alinexa  1578  alexn  1579  exanali  1585  19.26-2  1594  19.26-3an  1595  albiim  1611  2albiim  1612  ax12bOLD  1690  alrot3  1738  alrot4  1739  exrot3  1744  exrot4  1745  19.21-2  1864  nf2  1866  19.27  1869  19.28  1870  19.36  1871  19.37  1873  19.44  1877  19.45  1878  aaan  1884  eeor  1885  19.23vv  1892  pm11.53  1893  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  19.42vv  1907  19.42vvv  1908  4exdistr  1911  eean  1912  cbvex4v  2012  sbor  2066  sbrim  2067  sblim  2068  sban  2069  sbbi  2071  sblbis  2072  sbrbis  2073  sbrbif  2074  sbid2  2084  sbco2d  2087  sb8e  2093  sbnf2  2108  2sb5  2112  2sb6  2113  sbcom2  2114  sb6a  2116  2sb5rf  2117  2sb6rf  2118  sbex  2128  sbalv  2129  exsbOLD  2131  2exsb  2132  eujust  2206  euf  2210  cbveu  2224  eu2  2229  mo2  2233  sbmo  2234  mo3  2235  mo4f  2236  eu4  2243  moanim  2260  2mo  2282  2mos  2283  2eu1  2284  2eu3  2286  2eu4  2287  2eu6  2289  exists1  2293  abid  2341  eleq12i  2418  abeq2  2458  abeq2i  2460  clabel  2474  abid2f  2514  sbabel  2515  neeq12i  2528  necon1abii  2567  neanior  2601  ralnex  2624  rexnal  2625  ralinexa  2659  rexanali  2660  r3al  2671  r19.26-2  2747  ralbiim  2751  r19.30  2756  ralcomf  2769  rexcomf  2770  rexrot4  2774  reean  2777  3reeanv  2779  rabbi  2789  cbvralf  2829  cbvreu  2833  cbvral2v  2843  cbvrex2v  2844  cbvral3v  2845  cbvralsv  2846  cbvrexsv  2847  sbralie  2848  rabeq2i  2856  issetf  2864  2gencl  2888  3gencl  2889  ceqsex2  2895  ceqsex3v  2897  ceqsex6v  2899  ceqsex8v  2900  gencbvex  2901  spc3gv  2944  eqvincf  2967  ceqsrex2v  2974  elrab2  2996  ralab  2997  ralrab  2998  rexab  2999  rexrab  3000  ralab2  3001  rexab2  3003  eueq3  3011  morex  3020  euxfr2  3021  euxfr  3022  euind  3023  reu2  3024  reu6  3025  rmo4  3029  reu4  3030  reu7  3031  rmoim  3035  2reuswap  3038  reuind  3039  2reu5lem1  3041  2reu5lem2  3042  2reu5  3044  sbcco  3068  sbccomlem  3116  sbccom  3117  ra5  3130  rmo3  3133  csbco  3145  sbnfc2  3196  csbabg  3197  cbvralcsf  3198  cbvreucsf  3200  elsymdif  3223  dfss  3260  dfss2  3262  dfss2f  3264  ss2ab  3334  dfpss2  3354  dfpss3  3355  psseq12i  3360  sspsstri  3371  difeqri  3387  uneqri  3406  ssequn2  3436  unss  3437  rexun  3443  ralunb  3444  elin2  3446  ineqri  3449  dfss1  3460  dfss5  3461  nsspssun  3488  indifdir  3511  inrab2  3528  rabun2  3534  reuun2  3538  eq0  3564  0el  3566  abn0  3568  0pss  3588  disjr  3592  disj1  3593  disjpss  3601  undif4  3607  difin0ss  3616  inssdif0  3617  uneqdifeq  3638  r19.3rz  3641  r19.3rzv  3643  ralidm  3653  pwss  3736  dfpr2  3749  ralsns  3763  rexsns  3764  eltpg  3769  ralprg  3775  rexprg  3776  raltpg  3777  rextpg  3778  euabsn2  3791  eusn  3796  eldifsn  3839  rexdifsn  3843  difsnpss  3851  pwpw0  3855  ssunsn  3866  eqsn  3867  sstp  3870  tpss  3871  pwsnALT  3882  pwtp  3884  dfpss4  3888  eluniab  3903  elunirab  3904  unipr  3905  dfnfc2  3909  uniun  3910  uniin  3911  unissb  3921  elintab  3937  elintrab  3938  ssintab  3943  ssintrab  3949  intun  3958  intpr  3959  elrint  3967  iuncom4  3976  iuneq2  3985  dfiun2g  3999  ssiinf  4015  elriin  4038  iunxiun  4048  pwssb  4052  iunpwss  4055  ssofss  4076  axprimlem1  4088  axprimlem2  4089  axcnvprim  4091  axssetprim  4092  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  snex  4111  pwadjoin  4119  elopk  4129  1cex  4142  elpw1  4144  snelpw1  4146  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  0nel1c  4159  eqpw1  4162  pw1un  4163  pw111  4170  ssrelk  4211  eqrelk  4212  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  elp6  4263  opksnelsik  4265  opkelimagekg  4271  cnvkxpk  4276  inxpk  4277  elimaksn  4283  cokrelk  4284  xpkvexg  4285  cnvkexg  4286  p6exg  4290  ssetkex  4294  sikexlem  4295  sikexg  4296  dfimak2  4298  insklem  4304  ins2kexg  4305  ins3kexg  4306  dfidk2  4313  dfuni3  4315  dfint3  4318  ndisjrelk  4323  dfpw2  4327  cbviota  4344  dfiota4  4372  dfaddc2  4381  dfnnc2  4395  0nelsuc  4400  peano1  4402  peano2  4403  addccom  4406  peano5  4409  nnc0suc  4411  elsuc  4412  addcass  4414  elfin  4419  el0c  4420  nnsucelrlem1  4423  nnsucelrlem2  4424  nnsucelr  4427  nndisjeq  4428  preaddccan1lem1  4453  ltfinex  4464  ltfintrilem1  4465  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  ncfinlower  4483  nnpw1ex  4484  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  evenodddisj  4516  nnadjoinlem1  4519  nnadjoin  4520  nnpweqlem1  4522  nnpweq  4523  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  tfinnn  4534  spfinex  4537  spfinsfincl  4539  vfinspsslem1  4550  vfinspss  4551  vfinspclt  4552  vfinncsp  4554  dfphi2  4569  dfop2lem1  4573  dfop2lem2  4574  dfop2  4575  dfproj22  4577  phi011lem1  4596  phi011  4597  proj2op  4599  eqvinop  4604  copsex4g  4608  eqop  4609  phidisjnn  4613  cbvopab1  4624  brabga  4693  opelopabaf  4702  opabn0  4708  el1st  4721  br1stg  4722  setconslem1  4723  setconslem2  4724  setconslem3  4725  setconslem4  4726  setconslem6  4728  setconslem7  4729  df1st2  4730  elswap  4732  dfswap2  4733  dfima2  4737  dfco1  4740  dfsi2  4743  elima2  4747  elima3  4748  dfid3  4760  elxp  4795  opelxp  4805  brxp  4806  rabxp  4808  rexxp  4812  ralxpf  4813  rexxpf  4814  iunxpf  4815  xpundi  4818  xpundir  4819  elvvv  4825  brinxp2  4826  brinxp  4827  xp0r  4833  eqrelrel  4849  brswap2  4860  reliun  4865  reluni  4867  elcnv  4901  elcnv2  4902  cnvco  4906  elrn2  4909  eldm  4910  eldm2  4911  dmun  4924  dmin  4925  dmuni  4926  dmopab  4927  dmi  4931  elimapw1  4958  elimapw12  4959  elimapw13  4960  elimapw11c  4962  dfima3  4965  dfima4  4966  rnopab  4981  dmcoss  4985  dmcosseq  4987  rncoeq  4989  dmres  5000  resabs1  5007  elres  5010  dfres2  5017  imai  5025  epini  5036  cotr  5043  intasym  5045  intirr  5046  cnvopab  5047  cnvi  5049  imainss  5059  dfrel2  5079  dmsnn0  5084  rnsnn0  5085  dmsnopg  5086  cnvsn  5093  rnsnop  5095  dfrel3  5097  cnvresima  5103  dfco2  5107  dfco2a  5108  coundi  5109  coundir  5110  coiun  5117  coi1  5123  brcoi1  5125  relssdmrn  5129  relrelss  5130  dfcnv2  5133  elxp4  5141  df2nd2  5144  dfxp2  5146  cnviin  5151  dffun2  5152  dffun3  5153  dffun4  5154  dffun5  5155  dffun7  5167  dffun8  5168  dffun9  5169  nfunv  5172  funopab  5173  funun  5180  funsn  5181  funcnv  5190  fun2cnv  5192  fncnv  5194  fun11  5195  fununi  5196  imadif  5207  fnunsn  5227  fnres  5236  iunfopab  5241  fnopabg  5242  fnopab2g  5243  fun  5274  fcnvres  5281  dff12  5295  funforn  5315  dff1o2  5331  dff1o3  5332  dff1o5  5335  resdif  5346  ffoss  5354  f11o  5355  f1o00  5357  fo00  5358  elfv  5366  fv3  5381  nfvres  5392  fnrnfv  5404  dmfco  5421  eqfnfv3  5434  unpreima  5448  respreima  5450  fnasrn  5457  dff4  5461  dffo3  5462  dffo5  5464  ffnfvf  5468  fopabfv  5470  fsn2  5474  fconst3  5497  fconst4  5498  funfvima  5499  abrexco  5503  funiunfv  5507  dff13  5511  dff13f  5512  isocnv2  5532  isomin  5536  isoini  5537  opbr1st  5541  opbr2nd  5542  dfid4  5544  xpnedisj  5554  dmsi  5561  oprabid  5589  dfoprab2  5597  dmoprab  5614  rnoprab  5616  eloprabga  5620  resoprab  5623  ffnov  5629  fnov  5633  fov  5634  ovidig  5635  ov3  5641  ov6g  5642  foov  5648  ndmovcl  5656  ndmov  5657  ndmovdistr  5661  mptpreima  5722  mpt2mpt  5748  brsnsi  5803  brsnsi1  5805  brsnsi2  5806  brco1st  5807  brco2nd  5808  trtxp  5809  brtxp  5811  restxp  5815  elfix  5816  otelins2  5820  otelins3  5821  brimage  5822  oqelins4  5823  txpssvvv  5831  dmtxp  5832  otsnelsi3  5835  releqel  5837  releqopab  5838  releqmpt  5839  releqoprab  5840  releqmpt2  5841  cupex  5848  disjex  5851  addcfnex  5852  epprc  5855  funsex  5856  fnsex  5858  qrpprod  5860  brpprod  5864  dmpprod  5866  fnpprod  5869  brcrossg  5874  crossex  5876  pw1fnex  5878  pw1fnf1o  5881  fnfullfunlem1  5882  fvfullfunlem3  5889  clos1ex  5898  clos1conn  5901  clos1induct  5902  clos1is  5903  dfnnc3  5906  transex  5930  refex  5931  antisymex  5932  connexex  5933  foundex  5934  extex  5935  symex  5936  ersymtr  5952  porta  5953  sopc  5954  frds  5955  weds  5958  eqerlem  5980  qsexg  6002  qsid  6010  mapexi  6023  pmvalg  6030  mapval2  6038  enex  6052  xpassen  6077  enpw1lem1  6081  enmap2lem1  6083  enmap2lem4  6086  enmap1lem1  6089  enmap1lem4  6092  enpw1pw  6095  enprmaplem1  6096  enprmaplem4  6099  nenpw1pwlem1  6104  brltc  6134  lecex  6136  elncs  6140  elnc  6146  ovmuc  6151  mucex  6154  1cnc  6160  peano4nc  6171  ncssfin  6172  ncspw1eu  6180  ovcelem1  6192  ceexlem1  6194  ceex  6195  fnce  6197  ce0nnul  6198  ce0nn  6201  fce  6209  el2c  6212  lec0cg  6219  sbthlem1  6224  sbth  6227  addlec  6229  nc0le1  6237  leconnnc  6239  dflec3  6242  nclenc  6243  lenc  6244  tc11  6248  taddc  6249  letc  6251  tcfnex  6264  nclennlem1  6268  nnltp1clem1  6270  nmembers1lem1  6272  nncdiv3lem1  6275  nncdiv3lem2  6276  nncdiv3  6277  nnc3n3p1  6278  nnc3n3p2  6279  spacvallem1  6281  spacind  6287  spacis  6288  nchoicelem6  6294  nchoicelem8  6296  nchoicelem9  6297  nchoicelem10  6298  nchoicelem11  6299  nchoicelem12  6300  nchoicelem14  6302  nchoicelem16  6304  nchoicelem18  6306  nchoicelem19  6307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator