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  1373  falnanfal  1376  cadanOLD  1412  had0  1423  nic-axALT  1459  sbied  2160  sb6a  2215  sbelx  2228  sbco4  2238  mo  2345  2eu6  2419  abeq1i  2597  necon1bbii  2709  r19.41  2915  2ralor  2933  rexcom4a  3035  moeq  3173  2reuswap  3199  2reu5  3205  nfcdeq  3221  sbcid  3240  sbcco2  3247  sbc7  3251  sbcie2g  3257  eqsbc3  3263  sbcralt  3304  cbvralcsf  3356  cbvrabcsf  3359  abss  3458  ssab  3459  difrab  3660  neq0  3683  sbccsb  3736  vdif0  3773  difrab0eq  3774  ssunsn2  4058  sspr  4062  sstp  4063  prsspw  4071  uniintsn  4191  disjmoOLD  4303  brab1  4363  unopab  4393  axrep5  4434  axsep  4438  intexab  4473  reusv2lem4  4519  reusv2  4521  reuxfrd  4540  wefrc  4735  ordelord  4762  elvvv  4920  eliunxp  4999  ralxp  5003  rexxp  5004  opelco  5033  reldm0  5079  resieq  5143  iss  5177  imai  5204  cnvsym  5235  intasym  5236  asymref  5237  codir  5241  poirr2  5245  rninxp  5298  dffun3  5449  funopg  5470  fin  5608  f1cnvcnv  5631  funimass4  5758  fnressn  5909  resoprab  6198  mpt22eqb  6211  ov6g  6239  offval  6337  uniuni  6395  dfwe2  6403  orduniorsuc  6451  tfinds2  6484  resiexg  6524  dfopab2  6634  dfoprab3s  6635  fmpt2x  6646  fparlem1  6678  fparlem2  6679  brtpos0  6718  dftpos3  6729  tpostpos  6731  tz7.48lem  6860  omeu  6990  ercnv  7088  ixp0  7259  xpcomco  7363  xpassen  7367  php  7456  findcard3  7516  ixpfi2  7571  dfsup2  7614  card2on  7689  infeq5i  7758  cnfcom3lem  7827  r1elss  7899  rankxplim  7972  scott0s  7981  aceq1  8169  dfac5lem1  8175  dfac5lem2  8176  kmlem3  8203  kmlem8  8208  kmlem16  8216  cflem  8297  cf0  8302  alephval2  8618  rankcf  8823  r1tskina  8828  wfgru  8862  genpass  9057  psslinpr  9079  ltpsrpr  9155  infm3  10155  nnwos  10786  ioo0  11189  ico0  11210  ioc0  11211  icc0  11212  elfz2nn0  11336  elfzmlbp  11347  sqeqori  11827  hashgt12el  12022  hashgt12el2  12023  cshwidxmod  12287  clim0  12831  dvdslelem  13424  divalglem6  13449  isprm2lem  13617  pceu  13760  prmreclem2  13825  cshwshash  13978  isstruct  14031  xpscf  14345  acsfn2  14442  invsym2  14542  pospo  14984  efgrelexlemb  15991  gexex  16078  lssne0  16646  opsrtoslem1  17169  opsrtoslem2  17170  f1omvdco3  17606  psgnunilem5  17647  mdetunilem8  17897  ntreq0  18155  ordtrest2lem  18281  ist0-3  18423  ist1-2  18425  ist1-3  18427  cmpfi  18485  2ndcctbss  18533  ptbasfi  18628  ptcnplem  18668  hausdiag  18692  hauseqlcld  18693  cnmptcom  18725  txflf  19053  tgphaus  19161  metrest  19569  iccpnfcnv  19984  bcth3  20299  volun  20454  dyadmax  20505  vitalilem2  20516  vitalilem3  20517  mbfimaopnlem  20560  itg2leub  20639  dvres2  20814  ellogdm  21550  reasinsin  21757  leibpilem2  21802  ftalem3  21878  dchreq  22063  lnon0  23320  spansncvi  24177  pjssmii  24206  nmlnopgt0i  24523  largei  24793  cvexchlem  24894  xfree  24970  nmo  24997  2reuswap2  25000  fpwrelmapffslem  25162  addeq0  25165  eliccioo  25236  omndmul2  25307  ordtrest2NEWlem  25531  ordtconlem1  25533  xrge0iifcnv  25542  xrge0iifiso  25544  xrge0iifhom  25546  cntnevol  25822  eulerpartlemgh  25935  ballotlemfp1  26024  ballotlem7  26068  signswch  26113  derang0  26203  iccllyscon  26285  cvmsss2  26309  axacprim  26498  dftr6  26712  dfpo2  26717  opelco3  26742  elima4  26743  setinds2f  26745  elpotr  26747  tz6.26  26819  wfis2fg  26825  frins2fg  26861  wzel  26914  nobndlem1  26986  elfuns  27099  dfiota3  27107  imagesset  27137  axcontlem2  27243  lineunray  27420  ellines  27425  hfninf  27466  tan2h  27605  ovoliunnfl  27613  voliunnfl  27615  ftc1anc  27655  inixp  27802  heibor1lem  27890  tsna1  28098  4rexfrabdioph  28284  dford4  28526  islindf4  28648  isdomn3  28754  fgraphopab  28760  2rmoswap  29187  ndmaovcom  29290  rabasiun  29411  wlk0  29473  usgra2pth0  29483  rusgranumwlklem0  29747  frgra3v  29775  4cycl2vnunb  29790  vdn0frgrav2  29797  vdgn0frgrav2  29798  usg2spot2nb  29839  opelopab4  30106  2sb5nd  30115  un2122  30370  uunT12p4  30383  onfrALTlem5VD  30467  2sb5ndVD  30492  2sb5ndALT  30514  bnj446  30551  bnj563  30581  bnj110  30699  bnj153  30721  bnj557  30742  bnj864  30763  bnj865  30764  bnj849  30766  bnj929  30777  bnj1110  30821  bj-snglc  30952  sbelxNEW11  31164  ax11w14lemAUX11  31220  islshpat  31365  lkr0f  31442  lshpsmreu  31457  cvrnbtwn4  31627  ishlat2  31701  islvol5  31926  tendoeq2  33121  dibelval3  33495  mapdpglem3  34023  hdmapglem7a  34278
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