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

Theorem bitr4i 252
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
bitr4i.1
bitr4i.2
Assertion
Ref Expression
bitr4i

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2
2 bitr4i.2 . . 3
32bicomi 202 . 2
41, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  3bitr2i  273  3bitr2ri  274  3bitr4i  277  3bitr4ri  278  imor  412  dfbi2  628  pm5.32  636  imdistan  689  imimorb  877  nbi2  892  pm5.6  912  mpbiran  918  mpbiran2  919  biluk  933  3anrev  984  an3andi  1341  nancom  1346  nannanOLD  1349  nanbi  1352  xorneg  1375  casesifp  1392  cadan  1459  nic-ax  1506  nic-axALT  1507  19.43  1693  19.3v  1755  nf3  1961  nf4  1962  sb6x  2125  sb5f  2127  sb3an  2141  sbequ8ALT  2148  sb5  2174  sbhb  2182  sbnf2  2183  sbcom2  2189  eu1  2327  eu3OLD  2329  eu5OLD  2330  2moOLD  2374  2eu4OLD  2381  2eu6OLD  2384  cleqh  2572  cleqhOLD  2573  clelab  2601  cleqfOLD  2647  necon3bii  2725  neor  2781  neorian  2784  r2allem  2832  r2alfOLD  2834  r19.23t  2935  r2exfOLD  2979  r19.26-3  2986  r19.26m  2987  r19.43  3013  rabid2  3035  isset  3113  ralv  3123  rexv  3124  reuv  3125  rmov  3126  rexcom4b  3131  ceqsex4v  3150  ceqsex8v  3152  ceqsrexv  3233  ralrab2  3265  rexrab2  3267  reu2  3287  reu3  3289  reueq  3297  2reuswap  3302  reuind  3303  2reu5lem3  3307  sbc3an  3390  rmo2  3427  dfss2  3492  dfss3  3493  dfss3f  3495  ssabral  3570  rabss  3576  ssrabeq  3585  uniiunlem  3587  sspsstri  3605  npss  3613  uncom  3647  inass  3707  nsspssun  3730  dfss4  3731  dfun2  3732  dfin2  3733  indi  3743  indifdir  3753  difin2  3759  reupick3  3782  n0f  3793  eqv  3801  csbab  3855  vss  3863  disj  3867  disj3  3871  undisj1  3878  undisj2  3879  inundif  3906  undif  3908  exsnrex  4067  euabsn2  4101  euabsn  4102  raldifsni  4160  tppreqb  4171  pwpw0  4178  prssg  4185  ssunsn  4190  pwpr  4245  dfuni2  4251  unissb  4281  elint2  4293  ssint  4302  uniintab  4325  iuneq12df  4354  dfiin2g  4363  iunn0  4390  iunxun  4412  iunxiun  4413  iinpw  4419  disjor  4436  disjxiun  4449  dftr2  4547  dftr5  4548  dftr3  4549  dftr4  4550  vprc  4590  inuni  4614  eusv2  4651  reusv2lem4  4656  reusv6OLD  4663  reusv7OLD  4664  rexxfr  4672  snelpw  4698  sspwb  4701  pwssun  4791  dfid3  4801  dffr2  4849  dflim2  4939  orddif  4976  opthprc  5052  elxp3  5055  xpiundir  5060  elvv  5063  brinxp2  5066  relsn  5111  reliun  5128  inxp  5140  raliunxp  5147  cnvuni  5194  dm0rn0  5224  elrn  5248  ssdmres  5300  dfres2  5331  dfima2  5344  args  5370  dffr3  5374  cotrg  5383  intasym  5387  asymref  5388  intirr  5390  cnv0  5414  xpnz  5431  xp11  5447  xpimasn  5457  cnvresima  5501  resco  5516  rnco  5518  coiun  5522  coass  5531  cnvso  5551  dfiota2  5557  dffun2  5603  dffun6f  5607  dffun7  5619  dffun9  5621  funfn  5622  svrelfun  5656  dffn2  5737  dffn3  5743  fint  5769  dffn4  5806  dff1o4  5829  brprcneu  5864  eqfnfv3  5983  fnreseql  5997  fsn  6069  ftpg  6081  abrexco  6156  imaiun  6157  dff13  6166  isocnv2  6227  mpt22eqb  6411  elovmpt2  6520  sorpss  6585  abexex  6783  elxp6  6832  elxp7  6833  releldm2  6850  opiota  6859  fnmpt2  6868  frxp  6910  cnvimadfsn  6927  dftpos4  6993  tfrlem7  7071  ondif1  7170  oarec  7230  oeeu  7271  0er  7365  eroveu  7425  erovlem  7426  map0e  7476  elixpconst  7497  domen  7549  brsdom  7558  brdom2  7565  reuen1  7604  sbthlem10  7656  brsdom2  7661  xpf1o  7699  onfin2  7729  0sdom1dom  7737  modom  7740  unfi  7807  marypha2lem3  7917  dfsup2OLD  7923  wemapsolem  7996  sucprcreg  8046  elom3  8086  dfom5  8088  trcl  8180  epfrs  8183  rankf  8233  scottexs  8326  scott0s  8327  cplem1  8328  karden  8334  hta  8336  pm54.43lem  8401  alephsuc2  8482  iscard3  8495  aceq0  8520  aceq3lem  8522  dfac3  8523  dfac5lem2  8526  dfac5  8530  dfac7  8533  dfac12a  8549  kmlem12  8562  kmlem14  8564  kmlem15  8565  infmap2  8619  ackbij2  8644  dfacfin7  8800  ituniiun  8823  zorng  8905  brdom7disj  8930  entri2  8954  alephreg  8978  fpwwe2lem12  9040  fpwwe2lem13  9041  pwfseqlem1  9057  grutsk  9221  axgroth4  9231  grothprim  9233  grothtsk  9234  elni2  9276  ltsopi  9287  genpass  9408  psslinpr  9430  ltexprlem4  9438  ltresr  9538  1re  9616  infm3  10527  elnnz  10899  dfz2  10907  2rexuz  11162  nnwos  11178  eluz2b1  11182  qexALT  11226  elxr  11354  dflt2  11383  xrsupss  11529  xrinfmss  11530  elixx1  11567  elioo2  11599  elioopnf  11647  elicopnf  11649  elfz1  11706  fznn  11776  fzp1nel  11791  fznn0  11799  injresinj  11926  nn0opthlem1  12348  faclbnd4lem1  12371  hashf  12412  hashprdifel  12463  hashfun  12495  hashf1  12506  fz1isolem  12510  f1oun2prg  12865  shftdm  12904  rediv  12964  imdiv  12971  rexanre  13179  caubnd  13191  climreu  13379  prodmo  13743  dvdslelem  14030  bitsval  14074  smueqlem  14140  algcvgblem  14206  isprm2  14225  isprm3  14226  isprm4  14227  pythagtriplem2  14341  elgz  14449  hashbc0  14523  0ram  14538  isstruct  14642  issect  15148  isfull2  15280  isfth2  15284  fucinv  15342  eldmcoa  15392  isdrs  15563  fpwipodrs  15794  submacs  15996  isnsg4  16244  isgim  16310  gaorb  16345  oppgid  16391  oppgsubm  16397  oppgcntz  16399  ispgp  16612  efgsdm  16748  efgcpbllema  16772  iscyg2  16885  isring  17202  isirred2  17350  opprirred  17351  dfrhm2  17366  drngid2  17412  opprsubrg  17450  islmod  17516  lss1d  17609  islmhm  17673  islmim  17708  lbsextlem2  17805  lidlnz  17876  lidldvgen  17903  isnzr2  17911  isassa  17964  dfprm2  18524  dfprm2OLD  18527  isphl  18663  elocv  18699  iunocv  18712  isobs  18751  islinds  18844  1mavmul  19050  isbasis3g  19450  fctop  19505  cctop  19507  isclo2  19589  restsn  19671  lmbr  19759  ist0-3  19846  2ndcdisj  19957  1stccnp  19963  islocfin  20018  1stckgenlem  20054  txbas  20068  ptbasin  20078  tx2cn  20111  fbfinnfr  20342  fbasrn  20385  filuni  20386  ufinffr  20430  fin1aufil  20433  rnelfmlem  20453  flimrest  20484  alexsubALTlem3  20549  alexsubALTlem4  20550  tgphaus  20615  istlm  20687  iscusp2  20805  metuel2  21082  isngp2  21117  isnlm  21184  elcncf1di  21399  isphtpc  21494  phtpcer  21495  om1elbas  21532  isclm  21564  iscph  21617  iscau3  21717  minveclem3b  21843  elovolm  21886  ioombl1lem4  21971  dyaddisj  22005  vitali  22022  itg1climres  22121  itg2seq  22149  itg2monolem1  22157  itg2mono  22160  limcrcl  22278  lhop1  22415  itgsubst  22450  mdegleb  22464  isuc1p  22541  ismon1p  22543  plydivex  22693  ellogdm  23020  1cubr  23173  atandm2  23208  birthdaylem3  23283  dmarea  23287  dchrelbas2  23512  dchrelbas4  23518  axcontlem7  24273  nb3grapr  24453  nb3grapr2  24454  cusgrarn  24459  usgrasscusgra  24483  3v3e3cycl2  24664  wwlkextwrd  24728  isclwwlk  24768  erclwwlkref  24813  rusgranumwlkl1  24947  frgra3v  25002  2spotdisj  25061  numclwwlkovf2  25084  isgrpo2  25199  nmoubi  25687  nmobndseqi  25694  nmobndseqiOLD  25695  minvecolem1  25790  isch2  26141  hlimreui  26157  isch3  26159  ocsh  26201  dfch2  26325  spanuni  26462  nonbooli  26569  5oalem7  26578  adjsym  26752  elbdop2  26790  dmadjss  26806  nmopub  26827  nmfnleub  26844  nmop0h  26910  pjssposi  27091  pjordi  27092  cvbr2  27202  cvnbtwn2  27206  mdsl2i  27241  cvmdi  27243  elat2  27259  atom1d  27272  chirredi  27313  cdj3i  27360  or3di  27367  moel  27382  mo5f  27383  2reuswap2  27387  rexunirn  27390  rabid2f  27400  iuneq12daf  27425  iuninc  27428  disjorf  27440  disjunsn  27453  rabfmpunirn  27491  mptfnf  27499  funcnv5mpt  27511  eliccelico  27588  elicoelioo  27589  isomnd  27691  omndmul2  27702  isslmd  27745  hasheuni  28091  pwsiga  28130  sigainb  28136  2ndmbfm  28232  eulerpartlemgvv  28315  eulerpartlemgs2  28319  eulerpartlemn  28320  probun  28358  ballotlem2  28427  ballotlemodife  28436  erdszelem9  28643  erdszelem10  28644  pconcon  28676  cvmliftiota  28746  elmthm  28936  nepss  29095  dfso2  29183  dfpo2  29184  dfres3  29188  elrn3  29192  elima4  29209  elpotr  29213  dfon2lem3  29217  dfon2lem5  29219  dfon2lem7  29221  dfon2lem8  29222  predreseq  29259  cbvsetlike  29261  dffr4  29262  preduz  29280  wfi  29287  frind  29323  soseq  29334  wfrlem5  29347  wfrlem8  29350  wfrlem11  29353  elwlim  29379  wzel  29380  frrlem5  29391  frrlem5c  29393  elno3  29415  nosgnn0  29418  nocvxminlem  29450  nofulllem5  29466  symdifass  29477  brtxp2  29531  brpprod3a  29536  eltrans  29541  dfon3  29542  dffix2  29555  dffun10  29564  elfuns  29565  brsingle  29567  brimg  29587  brsuccf  29591  funpartfun  29593  funpartfv  29595  cgrxfr  29705  segletr  29764  outsideoftr  29779  df3nandALT1  29862  rabiun  30036  fin2solem  30039  ptrest  30048  ismblfin  30055  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  dvtanlem  30064  itg2addnclem2  30067  neifg  30189  filnetlem4  30199  fdc  30238  nninfnub  30244  prdstotbnd  30290  isdrngo1  30359  ispridl  30431  ismaxidl  30437  impor  30478  selconj  30500  mergeconj  30502  tradd  30507  scott0f  30577  prter1  30620  rexrabdioph  30727  dford4  30971  issdrg  31146  isdomn3  31164  lcmcllem  31202  pm11.52  31292  pm11.58  31296  pm13.192  31317  conss34  31351  bothtbothsame  32094  bothfbothsame  32095  aiffbtbat  32103  rmoanim  32184  2rmoswap  32189  isrng  32682  isrnghm  32698  rabeqsn  32919  rabsssn  32920  islindeps2  33084  isldepslvec2  33086  aacllem  33216  impexpdcom  33285  sbc3or  33302  opelopab4  33324  uunT12p1  33597  uunT12p2  33598  uunT12p3  33599  uun2221  33610  uun2221p1  33611  uun2221p2  33612  undif3VD  33682  onfrALTlem5VD  33685  bnj252  33755  bnj253  33756  bnj255  33757  bnj345  33766  bnj133  33780  bnj976  33836  bnj1098  33842  bnj121  33928  bnj130  33932  bnj150  33934  bnj581  33966  bnj607  33974  bnj865  33981  bnj917  33992  bnj934  33993  bnj964  34001  bnj983  34009  bnj996  34013  bnj1021  34022  bnj1033  34025  bnj1047  34029  bnj1049  34030  bnj1090  34035  bnj1128  34046  bnj1175  34060  bnj1189  34065  bnj1204  34068  bnj1253  34073  bnj1312  34114  bj-biexal3  34261  bj-sb5  34351  bj-cleqh  34358  bj-ralvw  34441  bj-rexvwv  34442  bj-rexcom4bv  34447  bj-rexcom4b  34448  bj-sbeq  34468  bj-inrab  34495  bj-xpima1snALT  34514  islshp  34704  islshpat  34742  lcvbr2  34747  lcvnbtwn2  34752  cvrnbtwn3  35001  isatl  35024  ishlat1  35077  ishlat2  35078  cvrat4  35167  pmapglbx  35493  lhpexle3  35736  dib1dim  36892  diblsmopel  36898  lcfls1lem  37261  bj-ifim123g  37706  bj-ifbibib  37721  bj-ifdfor  37722  bj-ifdfor2  37723  bj-ifdfan  37727  bj-ifdfbi  37730  snhesn  37809
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