MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr4i Unicode version

Theorem 3bitr4i 277
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3bitr4i.1
3bitr4i.2
3bitr4i.3
Assertion
Ref Expression
3bitr4i

Proof of Theorem 3bitr4i
StepHypRef Expression
1 3bitr4i.2 . 2
2 3bitr4i.1 . . 3
3 3bitr4i.3 . . 3
42, 3bitr4i 252 . 2
51, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  bibi2d  318  or4  528  pm4.14  578  pm4.71  630  pm5.32ri  638  an31  800  an4  824  orimdi  847  ordi  864  ordir  865  andir  868  dfbi3  893  orbidi  932  3anrot  978  3orrot  979  3ancoma  980  3orcoma  981  3orcomb  983  3ioran  991  3anbi123i  1185  3orbi123i  1186  an6  1308  3or6  1310  an33rean  1342  nancomOLD  1347  nanbi  1352  xorcom  1366  xorass  1367  xorneg2  1374  xorbi12i  1376  anxordi  1378  dfifp7  1387  ifpn  1391  hadbi  1454  hadcoma  1455  hadcomb  1456  cador  1458  cadan  1459  hadnot  1460  cadnot  1461  cadcoma  1462  cadcomb  1463  cad1  1465  nic-axALT  1507  stoic1a  1605  nfbii  1644  19.26-3an  1682  19.43OLD  1694  19.32v  1730  19.31v  1731  sbequ8  1744  19.42v  1775  4exdistr  1781  cbvexvw  1810  excom  1849  equsalhw  1945  19.32  1967  19.31  1968  19.42  1972  eeeanv  1989  cbvex  2022  cbvex2  2028  equsal  2036  dfsb3  2115  sbor  2139  sban  2140  sbbi  2142  sbnf2  2183  sbcom4  2190  sbex  2207  eu5  2310  sb8eu  2318  sb8euOLD  2319  sb8mo  2320  cbvmo  2322  eu1  2327  sbmo  2335  eqcomOLD  2467  abeq1  2582  cbvab  2598  cbvabOLD  2599  clelabOLD  2602  nfceqiOLD  2616  sbabel  2650  sbabelOLD  2651  r2allem  2832  r2alfOLD  2834  r19.21v  2862  ralbii2  2886  r3alOLD  2895  rexbii2  2957  r2exfOLD  2979  r19.30  3002  r19.32v  3003  r19.41v  3009  r19.41  3010  r19.42v  3012  r19.43  3013  ralcomf  3016  rexcomf  3017  reean  3024  3reeanv  3026  2ralor  3027  rabid2  3035  rabbi  3036  reubiia  3043  rmobiia  3048  reu5  3073  rmo5  3076  cbvralf  3078  cbvrexf  3079  cbvreu  3082  cbvrmo  3083  vjust  3110  ceqsex3v  3149  ceqsex4v  3150  ceqsex8v  3152  eueq  3271  reu2  3287  reu6  3288  reu3  3289  rmo4  3292  2reu5  3308  cbvsbc  3356  sbccomlem  3406  rmo3  3429  cbvralcsf  3466  cbvrexcsf  3467  cbvreucsf  3468  eqss  3518  uniiunlem  3587  sspsstri  3605  ssequn1  3673  unss  3677  rexun  3683  ralunb  3684  elin3  3689  incom  3690  inass  3707  ssin  3719  nssinpss  3729  dfun2  3732  difin  3734  indi  3743  indifdir  3753  symdif2  3763  rabn0  3805  csbabgOLD  3856  disj3  3871  ssdif0  3885  inssdif0  3895  ssundif  3911  dfif2  3943  eldifpr  4046  rexsns  4062  snprc  4093  reusn  4103  difsnpss  4173  prss  4184  tpss  4195  pwpr  4245  eluni2  4253  elunirab  4261  uniun  4268  unissb  4281  elintrab  4298  ssintrab  4310  intun  4319  intpr  4320  iuncom  4337  iuncom4  4338  iunab  4376  ssiinf  4379  iunn0  4390  iinab  4391  iunin2  4394  iinun2  4396  iundif2  4397  iunun  4411  iunxun  4412  iunxiun  4413  sspwuni  4416  iinpw  4419  cbvdisj  4432  disjor  4436  brun  4500  brin  4501  brdif  4502  dftr2  4547  intexrab  4611  inuni  4614  reusv5OLD  4662  reusv7OLD  4664  ssext  4707  pweqb  4709  otth2  4733  opelopabsbALT  4761  eqopab2b  4782  pwin  4789  pwun  4793  dflim2  4939  unisuc  4959  xpiundi  5059  xpiundir  5060  poinxp  5068  soinxp  5069  frinxp  5070  seinxp  5071  weinxp  5072  inopab  5138  difopab  5139  raliunxp  5147  rexiunxp  5148  rexxpf  5155  iunxpf  5156  cnvco  5193  dmiun  5216  dmuni  5217  dm0rn0  5224  brres  5285  dmres  5299  restidsing  5335  cnvsym  5386  asymref  5388  codir  5392  qfto  5393  cnvopab  5412  cnvdif  5417  rniun  5421  dminss  5425  imainss  5426  difxp  5436  xpdifid  5440  dmsnn0  5478  cnvcnvsn  5490  resco  5516  imaco  5517  rnco  5518  coiun  5522  coass  5531  ressn  5548  cnviin  5549  cnvpo  5550  cnvso  5551  xpco  5552  funcnv  5653  funcnv3  5654  fncnv  5657  fun11  5658  imadif  5668  fnres  5702  dfmpt3  5708  fnopabg  5709  fint  5769  fin  5770  fores  5809  dff1o3  5827  f1ompt  6053  fsn  6069  imaiun  6157  isocnv2  6227  isocnv3  6228  isores2  6229  isomin  6233  eqoprab2b  6355  sucexb  6644  sucelon  6652  dflim4  6683  fun11iun  6760  f11o  6762  opabex3d  6778  opabex3  6779  dfopab2  6854  dfoprab3s  6855  fmpt2x  6866  fparlem1  6900  fparlem2  6901  fsplit  6905  suppvalbr  6922  tpostpos  6994  dfsmo2  7037  brwitnlem  7176  oarec  7230  qsid  7396  uniinqs  7410  mapval2  7468  mapsncnv  7485  elixp2  7493  ixpin  7514  brsdom  7558  brdom2  7565  xpassen  7631  brsdom2  7661  unfilem1  7804  fiint  7817  dfsup2  7922  supmo  7932  rankc1  8309  cp  8330  isinfcard  8494  aceq1  8519  aceq2  8521  dfac5lem3  8527  dfac10b  8540  dfac12a  8549  dffin7-2  8799  dfacfin7  8800  fin1a2lem6  8806  iunfo  8935  konigthlem  8964  axgroth6  9227  axgroth3  9230  sstskm  9241  ltexprlem1  9435  gt0srpr  9476  ltpsrpr  9507  map2psrpr  9508  ltresr  9538  fimaxre3  10517  sup3  10525  supmul1  10533  elnn0z  10902  elznn0nn  10903  zmin  11207  xrnemnf  11357  xrnepnf  11358  elioomnf  11648  elxrge0  11658  elfzuzb  11711  fzass4  11750  elfz2nn0  11798  elfzo2  11832  elfzo3  11844  lbfzo0  11862  fzind2  11924  nn0opthlem1  12348  rexfiuz  13180  fsumcom2  13589  prodmo  13743  fprodcom2  13788  sinltx  13924  divalglem4  14054  divalglem10  14060  isprm2lem  14224  4sqlem12  14474  imasleval  14938  xpsfrnel  14960  xpscf  14963  isssc  15189  isffth2  15285  ispos2  15577  ismhm  15968  nsgacs  16237  isgim  16310  oppgcntz  16399  f1omvdco3  16474  pmtrprfvalrn  16513  efgrelexlemb  16768  pgpfac1  17131  pgpfac  17135  issrg  17159  opprsubg  17285  opprunit  17310  isirred2  17350  opprirred  17351  drngprop  17407  opprdrng  17420  islss  17581  islbs  17722  isdomn2  17948  unocv  18711  iunocv  18712  fvmptnn04if  19350  istps2OLD  19422  isbasis2g  19449  tgval2  19457  ntreq0  19578  isclo2  19589  cmpcov2  19890  is1stc2  19943  1stcelcls  19962  llyi  19975  unisngl  20028  txuni2  20066  xkobval  20087  hausdiag  20146  isfbas2  20336  elfg  20372  fbasrn  20385  fmfnfmlem3  20457  isfcls  20510  alexsubALTlem2  20548  istmd  20573  istgp  20576  istrg  20666  istdrg  20668  istdrg2  20680  isms2  20953  metuel2  21082  restmetu  21090  isngp  21116  isngp2  21117  isngp3  21118  elii1  21435  iscph  21617  isbn  21777  pmltpc  21862  ovolfcl  21878  finiunmbl  21954  iundisj  21958  dyaddisj  22005  vitalilem1  22017  ellimc3  22283  ig1pval3  22575  plyun0  22594  plydivex  22693  aannenlem2  22725  ellogrn  22947  atandm  23207  atandm3  23209  atans2  23262  colinearalg  24213  axeuclid  24266  usgreg2spot  25067  issubgo  25305  h2hlm  25897  issh  26125  chcon2i  26382  chcon1i  26383  chcon3i  26384  chnlei  26403  cmcm2i  26511  cmcm3i  26512  3oalem3  26582  pjdifnormii  26601  pjneli  26641  dfadj2  26804  cnvadj  26811  hhcno  26823  hhcnf  26824  eleigvec  26876  eleigvec2  26877  pjimai  27095  isst  27132  ishst  27133  cvnbtwn4  27208  chrelat4i  27292  moel  27382  rmo3f  27394  rmo4fOLD  27395  rabid2f  27400  disjnf  27433  cbvdisjf  27434  disjorf  27440  iundisjf  27448  disjexc  27452  mptfnf  27499  xrdifh  27591  iundisjfi  27601  xrnarchi  27728  isorng  27789  cmpcref  27853  ordtconlem1  27906  isrrext  27981  cntnevol  28199  ddemeas  28208  eulerpartleme  28302  eulerpartlemv  28303  eulerpartlemt0  28308  eulerpartlemgvv  28315  eulerpartlemn  28320  ballotlem2  28427  ballotlemodife  28436  erdszelem1  28635  cvmliftlem15  28743  snmlval  28776  elmpst  28896  mpstrcl  28901  untuni  29081  dfso3  29097  dftr6  29179  coep  29180  coepr  29181  dffr5  29182  dfso2  29183  dfpo2  29184  cnvco1  29189  cnvco2  29190  eldm3  29191  socnv  29194  dfdm5  29206  dfrn5  29207  wfrlem8  29350  wfrlem11  29353  frrlem5c  29393  elno3  29415  nofulllem5  29466  elsymdif  29473  symdifass  29477  brsset  29539  idsset  29540  dfon3  29542  dfbigcup2  29549  dfom5b  29562  dffun10  29564  dfiota3  29573  fnimage  29579  brdomain  29583  brrange  29584  brimg  29587  brapply  29588  brcup  29589  brcap  29590  funpartlem  29592  brrestrict  29599  tfrqfree  29601  brub  29604  altopelaltxp  29626  df3nandALT1  29862  imnand2  29865  iundif1  30037  supaddc  30041  ismblfin  30055  mbfposadd  30062  itg2addnclem2  30067  ftc1anc  30098  trer  30134  filnetlem4  30199  inixp  30219  prdstotbnd  30290  heibor1lem  30305  isrngohom  30368  isidl  30411  isfldidl2  30466  isdmn3  30471  sbccom2lem  30529  moxfr  30624  fphpd  30750  issdrg2  31147  undisjrab  31186  nzss  31222  pm10.541  31272  compab  31350  conss34  31351  r19.32  32172  rmoanim  32184  usgra2pth0  32355  ismgmhm  32471  issubmgm  32477  sgrp2sgrp  32552  islindeps  33054  elsymdifxor  33217  onfrALTlem5  33314  bnj257  33759  bnj268  33761  bnj290  33762  bnj312  33764  bnj89  33774  bnj538OLD  33797  bnj887  33823  bnj976  33836  bnj1019  33838  bnj1146  33850  bnj1385  33891  bnj110  33916  bnj121  33928  bnj130  33932  bnj153  33938  bnj543  33951  bnj580  33971  bnj607  33974  bnj849  33983  bnj882  33984  bnj916  33991  bnj985  34011  bnj1033  34025  bnj1083  34034  bnj1090  34035  bnj1128  34046  bnj1174  34059  bnj1228  34067  bj-dfbi5  34155  bj-nfn  34219  bj-cbvexv  34297  bj-cbvex2v  34303  bj-equsalv  34309  bj-equsalvv  34310  bj-abeq1  34360  bj-vjust  34372  bj-sbnf  34412  bj-ralcom4  34444  bj-csbsnlem  34470  pmapglbx  35493  lhpexle3  35736  cdleme25cv  36084  dicelval3  36907  diclspsn  36921  lcfls1c  37263  bj-ifid2  37711  bj-ifim1  37712  bj-ifim2  37713  bj-ifnot  37717  bj-ifnot23  37718  bj-ifananb  37731  bj-ifxorxorb  37733  bj-ifnannanb  37735  rp-fakeinunass  37740  elintima  37765  cotr2g  37786  frege54cor0a  37890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator