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

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

Proof of Theorem bitr3i
StepHypRef Expression
1 bitr3i.1 . . 3
21bicomi 202 . 2
3 bitr3i.2 . 2
42, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  3bitrri  272  3bitr3i  275  3bitr3ri  276  xchnxbi  308  ianor  488  orordi  530  orordir  531  anandi  828  anandir  829  trunantru  1437  falnanfal  1440  had0  1471  nic-axALT  1507  sbied  2151  sbidm  2156  sb6a  2192  sbelx  2202  sbco4  2210  mo  2325  2eu6  2383  2eu6OLD  2384  bm1.1  2440  abeq1iOLD  2587  cbvab  2598  necon1bbiiOLD  2722  nabbi  2790  r19.41v  3009  r19.41  3010  2ralor  3027  rexcom4a  3130  moeq  3275  2reuswap  3302  2reu5  3308  nfcdeq  3324  sbcid  3344  sbcco2  3351  sbc7  3355  sbcie2g  3361  eqsbc3  3367  sbcralt  3408  cbvralcsf  3466  cbvrabcsf  3469  abss  3568  ssab  3569  difrab  3771  neq0  3795  sbccsb  3849  vdif0  3886  difrab0eq  3887  ssunsn2  4189  sspr  4193  sstp  4194  prsspwOLD  4203  uniintsn  4324  rabasiun  4334  disjmoOLD  4437  brab1  4497  unopab  4527  axrep5  4568  axsep  4572  intexab  4610  reusv2lem4  4656  reusv2  4658  reuxfrd  4677  wefrc  4878  ordelord  4905  elvvv  5064  eliunxp  5145  ralxp  5149  rexxp  5150  opelco  5179  reldm0  5225  resieq  5289  iss  5326  imai  5354  cnvsym  5386  intasym  5387  asymref  5388  codir  5392  poirr2  5396  xpdifid  5440  rninxp  5451  dffun3  5604  funopg  5625  fin  5770  f1cnvcnv  5794  funimass4  5924  fnressn  6083  resoprab  6398  mpt22eqb  6411  elrnmpt2res  6416  ov6g  6440  offval  6547  uniuni  6609  dfwe2  6617  orduniorsuc  6665  tfinds2  6698  resiexg  6736  dfopab2  6854  dfoprab3s  6855  fmpt2x  6866  fparlem1  6900  fparlem2  6901  brtpos0  6981  dftpos3  6992  tpostpos  6994  tz7.48lem  7125  omeu  7253  ercnv  7351  ixp0  7522  xpcomco  7627  xpassen  7631  php  7721  findcard3  7783  ixpfi2  7838  dfsup2  7922  card2on  8001  infeq5i  8074  cnfcom3lem  8168  cnfcom3lemOLD  8176  r1elss  8245  rankxplim  8318  scott0s  8327  aceq1  8519  dfac5lem1  8525  dfac5lem2  8526  kmlem3  8553  kmlem8  8558  kmlem16  8566  cflem  8647  cf0  8652  alephval2  8968  rankcf  9176  r1tskina  9181  wfgru  9215  genpass  9408  psslinpr  9430  ltpsrpr  9507  infm3  10527  nnwos  11178  ioo0  11583  ico0  11604  ioc0  11605  icc0  11606  elfz2nn0  11798  elfzmlbp  11815  sqeqori  12280  hashgt12el  12481  hashgt12el2  12482  cshwidxmod  12774  clim0  13329  divalglem6  14056  isprm2lem  14224  pceu  14370  prmreclem2  14435  cshwshash  14589  isstruct  14642  xpscf  14963  acsfn2  15060  invsym2  15157  pospo  15603  f1omvdco3  16474  psgnunilem5  16519  efgrelexlemb  16768  gexex  16859  srgrmhm  17187  lssne0  17597  opsrtoslem1  18148  opsrtoslem2  18149  islindf4  18873  mdetunilem8  19121  cpmatmcllem  19219  pmatcollpw2lem  19278  ntreq0  19578  ordtrest2lem  19704  ist0-3  19846  ist1-2  19848  ist1-3  19850  cmpfi  19908  2ndcctbss  19956  ptbasfi  20082  ptcnplem  20122  hausdiag  20146  hauseqlcld  20147  cnmptcom  20179  txflf  20507  tgphaus  20615  metrest  21027  iccpnfcnv  21444  bcth3  21770  volun  21955  dyadmax  22007  vitalilem2  22018  vitalilem3  22019  mbfimaopnlem  22062  itg2leub  22141  dvres2  22316  ellogdm  23020  reasinsin  23227  leibpilem2  23272  ftalem3  23348  dchreq  23533  legso  23985  axcontlem2  24268  rusgranumwlklem0  24948  frgra3v  25002  4cycl2vnunb  25017  vdn0frgrav2  25023  vdgn0frgrav2  25024  usg2spot2nb  25065  lnon0  25713  spansncvi  26570  pjssmii  26599  nmlnopgt0i  26916  largei  27186  cvexchlem  27287  xfree  27363  spc2ed  27372  nmo  27384  2reuswap2  27387  fpwrelmapffslem  27555  addeq0  27558  eliccioo  27627  qtophaus  27839  ordtrest2NEWlem  27904  ordtconlem1  27906  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  cntnevol  28199  eulerpartlemgh  28317  ballotlemfp1  28430  ballotlem7  28474  signswch  28518  derang0  28613  iccllyscon  28695  cvmsss2  28719  elmrsubrn  28880  quad3  29024  axacprim  29079  dftr6  29179  dfpo2  29184  opelco3  29208  elima4  29209  setinds2f  29211  elpotr  29213  tz6.26  29285  wfis2fg  29291  frins2fg  29327  wzel  29380  nobndlem1  29452  elfuns  29565  dfiota3  29573  imagesset  29603  lineunray  29797  ellines  29802  hfninf  29843  finixpnum  30038  fin2so  30040  tan2h  30047  ovoliunnfl  30056  voliunnfl  30058  ftc1anc  30098  inixp  30219  heibor1lem  30305  csbcom2fi  30534  tsna1  30551  4rexfrabdioph  30731  dford4  30971  isdomn3  31164  fgraphopab  31170  undisjrab  31186  radcnvrat  31195  ellimcabssub0  31623  fourierdlem42  31931  2rmoswap  32189  ndmaovcom  32290  usgra2pth0  32355  euelss  32553  eliunxp2  32923  pgrpgt2nabl  32959  islindeps  33054  lindslinindsimp1  33058  lindslinindsimp2  33064  opelopab4  33324  2sb5nd  33333  un2122  33587  uunT12p4  33600  onfrALTlem5VD  33685  2sb5ndVD  33710  2sb5ndALT  33732  bnj446  33769  bnj563  33800  bnj110  33916  bnj153  33938  bnj864  33980  bnj865  33981  bnj849  33983  bnj929  33994  bnj1110  34038  bj-axrep5  34378  bj-axsep  34379  bj-rexcom4a  34446  bj-snglc  34527  islshpat  34742  lkr0f  34819  lshpsmreu  34834  cvrnbtwn4  35004  ishlat2  35078  islvol5  35303  tendoeq2  36500  dibelval3  36874  mapdpglem3  37402  hdmapglem7a  37657  bj-ifim123g  37706  bj-ifbibib  37721
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