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

Theorem bitr3i 244
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3i.1
bitr3i.2
Assertion
Ref Expression
bitr3i

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3
21bicomi 195 . 2
3 bitr3i.2 . 2
42, 3bitri 242 1
Colors of variables: wff set class
Syntax hints:  <->wb 178
This theorem is referenced by:  3bitrri  265  3bitr3i  268  3bitr3ri  269  xchnxbi  301  ianor  476  orordi  518  orordir  519  anandi  803  anandir  804  trunantru  1364  falnanfal  1367  cadan  1402  had0  1413  nic-axALT  1449  sbied  2161  sbelx  2212  2eu6  2377  abeq1i  2555  necon1bbii  2667  r19.41  2871  2ralor  2888  rexcom4a  2989  moeq  3123  2reuswap  3149  2reu5  3155  nfcdeq  3171  sbcid  3190  sbcco2  3197  sbc7  3201  sbcie2g  3207  eqsbc3  3213  sbcralt  3253  cbvralcsf  3304  cbvrabcsf  3307  abss  3405  ssab  3406  difrab  3607  neq0  3630  sbccsb  3683  vdif0  3717  difrab0eq  3718  ssunsn2  3990  sspr  3994  sstp  3995  prsspw  4003  uniintsn  4120  disjmoOLD  4232  brab1  4292  unopab  4322  axrep5  4363  axsep  4367  intexab  4401  wefrc  4621  ordelord  4648  uniuni  4761  reusv2lem4  4772  reusv2  4774  reuxfrd  4793  dfwe2  4807  orduniorsuc  4855  tfinds2  4888  elvvv  4981  eliunxp  5058  ralxp  5062  rexxp  5063  opelco  5090  reldm0  5135  resieq  5204  resiexg  5236  iss  5237  imai  5264  cnvsym  5296  intasym  5297  asymref  5298  codir  5302  poirr2  5306  rninxp  5358  dffun3  5516  funopg  5536  fin  5674  f1cnvcnv  5698  funimass4  5829  fnressn  5970  resoprab  6220  mpt22eqb  6233  ov6g  6265  offval  6366  dfopab2  6455  dfoprab3s  6456  fmpt2x  6471  fparlem1  6500  fparlem2  6501  brtpos0  6540  dftpos3  6551  tpostpos  6553  tz7.48lem  6751  omeu  6881  ercnv  6979  ixp0  7148  xpcomco  7251  xpassen  7255  php  7344  findcard3  7403  ixpfi2  7458  dfsup2  7500  card2on  7575  infeq5i  7644  cnfcom3lem  7713  r1elss  7785  rankxplim  7858  scott0s  7867  aceq1  8053  dfac5lem1  8059  dfac5lem2  8060  kmlem3  8087  kmlem8  8092  kmlem16  8100  cflem  8181  cf0  8186  alephval2  8502  rankcf  8707  r1tskina  8712  wfgru  8746  genpass  8941  psslinpr  8963  ltpsrpr  9039  infm3  10022  nnwos  10599  ioo0  10996  ico0  11017  ioc0  11018  icc0  11019  elfz2nn0  11137  sqeqori  11548  hashgt12el  11737  hashgt12el2  11738  clim0  12355  dvdslelem  12949  divalglem6  12973  isprm2lem  13141  pceu  13275  prmreclem2  13340  isstruct  13534  xpscf  13846  acsfn2  13943  invsym2  14043  pospo  14485  efgrelexlemb  15418  gexex  15504  lssne0  16063  opsrtoslem1  16580  opsrtoslem2  16581  ntreq0  17177  ordtrest2lem  17303  ist0-3  17445  ist1-2  17447  ist1-3  17449  cmpfi  17507  2ndcctbss  17554  ptbasfi  17649  ptcnplem  17689  hausdiag  17713  hauseqlcld  17714  cnmptcom  17746  txflf  18074  tgphaus  18182  metrest  18590  iccpnfcnv  19005  bcth3  19320  volun  19475  dyadmax  19526  vitalilem2  19537  vitalilem3  19538  mbfimaopnlem  19581  itg2leub  19660  dvres2  19835  ellogdm  20566  reasinsin  20772  leibpilem2  20817  ftalem3  20893  dchreq  21078  lnon0  22335  spansncvi  23190  pjssmii  23219  nmlnopgt0i  23536  largei  23806  cvexchlem  23907  xfree  23983  nmo  24011  2reuswap2  24014  fpwrelmapffslem  24183  addeq0  24186  eliccioo  24253  omndmul2  24317  xrge0iifcnv  24532  xrge0iifiso  24534  xrge0iifhom  24536  cntnevol  24812  eulerpartlemgh  24920  ballotlemfp1  25009  ballotlem7  25053  derang0  25115  iccllyscon  25197  cvmsss2  25221  axacprim  25416  dftr6  25633  dfpo2  25638  opelco3  25663  elima4  25664  setinds2f  25666  elpotr  25668  tz6.26  25740  wfis2fg  25746  frins2fg  25782  wzel  25835  nobndlem1  25907  elfuns  26020  dfiota3  26028  imagesset  26058  axcontlem2  26164  lineunray  26341  ellines  26346  hfninf  26387  tan2h  26505  ovoliunnfl  26513  voliunnfl  26515  ftc1anc  26555  inixp  26697  heibor1lem  26785  tsna1  26993  4rexfrabdioph  27193  dford4  27435  islindf4  27620  f1omvdco3  27704  psgnunilem5  27729  isdomn3  27835  fgraphopab  27841  2rmoswap  28272  ndmaovcom  28380  elfzmlbp  28450  cshwssize  28644  usgra2pth0  28670  frgra3v  28786  4cycl2vnunb  28801  vdn0frgrav2  28808  vdgn0frgrav2  28809  usg2spot2nb  28848  opelopab4  29033  2sb5nd  29042  un2122  29297  uunT12p4  29310  onfrALTlem5VD  29394  2sb5ndVD  29419  2sb5ndALT  29441  bnj446  29478  bnj563  29508  bnj110  29626  bnj153  29648  bnj557  29669  bnj864  29690  bnj865  29691  bnj849  29693  bnj929  29704  bnj1110  29748  sbelxNEW7  30010  ax7w14lemAUX7  30066  islshpat  30211  lkr0f  30288  lshpsmreu  30303  cvrnbtwn4  30473  ishlat2  30547  islvol5  30772  tendoeq2  31967  dibelval3  32341  mapdpglem3  32869  hdmapglem7a  33124
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 179
  Copyright terms: Public domain W3C validator