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

Theorem 3bitri 271
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
3bitri.1
3bitri.2
3bitri.3
Assertion
Ref Expression
3bitri

Proof of Theorem 3bitri
StepHypRef Expression
1 3bitri.1 . 2
2 3bitri.2 . . 3
3 3bitri.3 . . 3
42, 3bitri 249 . 2
51, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  bibi1i  314  orbi1i  520  orass  524  or32  527  pm5.32  636  an32  798  cases  970  an3andi  1341  an33rean  1342  excxor  1368  trunanfal  1438  falxortru  1443  cadan  1459  nic-axALT  1507  tbw-bijust  1531  rb-bijust  1582  19.43  1693  19.43OLD  1694  19.12vvv  1765  3exdistr  1780  excom13  1851  nf4  1962  19.12vv  1986  eeeanv  1989  ee4anv  1990  sbn  2132  sb3an  2141  sbnf2  2183  sbcom2  2189  sbel2x  2203  sbco4  2210  2sb8e  2211  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  sb8eu  2318  sb8euOLD  2319  2mo2  2372  2eu4OLD  2381  2eu7  2385  2eu8  2386  r19.23v  2937  r19.26-3  2986  rexcom13  3020  cbvreu  3082  ceqsex2  3147  ceqsex4v  3150  ralrab2  3265  rexrab2  3267  reu2  3287  rmo4  3292  reu8  3295  2reu5lem3  3307  sbc3an  3390  rmo2  3427  rmo3  3429  dfss2  3492  ss2rab  3575  rabss  3576  ssrab  3577  dfss4  3731  undi  3744  undif3  3758  difin2  3759  dfnul2  3786  disj  3867  disj4  3875  disjsn  4090  raldifsni  4160  ssunpr  4192  sspr  4193  sstp  4194  uni0b  4274  uni0c  4275  ssint  4302  iunss  4371  iundif2  4397  disjor  4436  reusv2lem4  4656  nfnid  4681  ssextss  4706  eqvinop  4736  opcom  4746  opeqsn  4748  opeqpr  4749  brabsb  4763  opelopabf  4777  dfid3  4801  pofun  4821  sotrieq  4832  opeliunxp  5056  xpiundi  5059  brinxp2  5066  ssrel  5096  reliun  5128  exopxfr  5151  cnvuni  5194  dmopab3  5220  opelres  5284  elres  5314  elsnres  5315  asymref2  5389  intirr  5390  xpeq0  5432  xpdifid  5440  ssrnres  5450  dminxp  5452  dfrel4v  5463  dmsnn0  5478  rnco  5518  coeq0  5521  sb8iota  5563  dffun2  5603  fun11  5658  isarep1  5672  dff1o4  5829  opabiota  5936  fvopab5  5979  fvn0ssdmfun  6022  fnressn  6083  f13dfv  6180  dff1o6  6181  fliftel  6207  oprabid  6323  mpt22eqb  6411  ralrnmpt2  6417  uniuni  6609  dflim3  6682  dfom2  6702  elxp4  6744  elxp5  6745  opabex3d  6778  opabex3  6779  el2xptp  6843  xporderlem  6911  tz7.48lem  7125  seqomlem2  7135  oaord  7215  oeeu  7271  nnaord  7287  ecid  7395  mptelixpg  7526  elixpsn  7528  mapsnen  7613  xpsnen  7621  xpcomco  7627  xpassen  7631  omxpenlem  7638  dom0  7665  modom  7740  dfsup2OLD  7923  tz9.12lem3  8228  rankxpsuc  8321  cp  8330  cardprclem  8381  infxpenlem  8412  dfac5lem1  8525  dfac5lem2  8526  dfac5lem5  8529  dfac10c  8539  kmlem3  8553  kmlem12  8562  kmlem13  8563  kmlem14  8564  kmlem15  8565  ackbij2  8644  cflim2  8664  dffin7-2  8799  dfacfin7  8800  fin1a2lem12  8812  axdc3lem3  8853  cfpwsdom  8980  recmulnq  9363  genpass  9408  psslinpr  9430  suplem2pr  9452  opelreal  9528  ltxrlt  9676  addid1  9781  fimaxre  10515  elnn0  10822  elnn0z  10902  nnwos  11178  elxr  11354  xrnepnf  11358  elfzuzb  11711  4fvwrd4  11822  elfzo2  11832  ssnn0fi  12094  sqeqori  12280  fsumcom2  13589  modfsummod  13608  fprodcom2  13788  rpnnen2  13959  gcdcllem1  14149  isprm2  14225  pythagtriplem2  14341  infpn2  14431  4sqlem12  14474  eldmcoa  15392  oduposb  15766  gsumwspan  16014  isnsg2  16231  isnsg4  16244  efgcpbllemb  16773  dmdprd  17029  dprdval  17034  dprdvalOLD  17036  dprdw  17043  dprdwOLD  17050  dprd2d2  17093  dfrhm2  17366  brric2  17394  issubrg  17429  islmim  17708  lbsextlem2  17805  opsrtoslem1  18148  pjfval2  18740  fvmptnn04if  19350  istps3OLD  19423  ntreq0  19578  cmpsub  19900  2ndcdisj  19957  unisngl  20028  txbas  20068  elpt  20073  txkgen  20153  xkococn  20161  fbun  20341  trfil2  20388  fin1aufil  20433  alexsubALTlem3  20549  cnextcn  20567  qustgplem  20619  eltsms  20631  ustn0  20723  fmucndlem  20794  metrest  21027  restmetu  21090  srabn  21800  ellogdm  23020  1cubr  23173  leibpilem2  23272  dmarea  23287  vmasum  23491  dchrelbas2  23512  ltgov  23983  axlowdimlem13  24257  axeuclidlem  24265  trls  24538  4cycl4v4e  24666  4cycl4dv4e  24668  el2wlkonotot0  24872  usg2spthonot0  24889  frgra3v  25002  usg2spot2nb  25065  frgrareg  25117  frgraregord013  25118  h2hcau  25896  h2hlm  25897  axhcompl-zf  25915  shlesb1i  26304  shne0i  26366  chnlei  26403  cmbr2i  26514  pjneli  26641  ho02i  26748  adjsym  26752  adjeu  26808  lnopeqi  26927  largei  27186  atoml2i  27302  cdj3lem3b  27359  or3di  27367  mo5f  27383  rmo3f  27394  rmo4fOLD  27395  disjnf  27433  disjorf  27440  ssrelf  27466  ofpreima  27507  disjdsct  27521  1stpreima  27524  2ndpreima  27525  f1od2  27547  xrdifh  27591  nndiffz1  27596  ordtconlem1  27906  ind1a  28034  measiuns  28188  elunirnmbfm  28224  eulerpartlemr  28313  eulerpartlemgh  28317  eulerpartlemn  28320  ballotlemodife  28436  cvmlift2lem1  28747  elmthm  28936  quad3  29024  3orit  29092  brtp  29178  dftr6  29179  dfpo2  29184  eldm3  29191  elrn3  29192  elima4  29209  19.12b  29234  sspred  29252  predreseq  29259  preduz  29280  wfi  29287  frind  29323  nofulllem5  29466  brtxp  29530  brtxp2  29531  brpprod  29535  brpprod3a  29536  elfix  29553  dffix2  29555  ellimits  29560  dffun10  29564  elfuns  29565  elsingles  29568  brimg  29587  brapply  29588  brsuccf  29591  funpartlem  29592  brrestrict  29599  dfrdg4  29600  tfrqfree  29601  brlb  29605  altopthc  29621  altopthd  29622  fvtransport  29682  hfext  29840  df3nandALT2  29863  areacirclem5  30111  nn0prpw  30141  filnetlem4  30199  isbnd2  30279  sbcalf  30517  sbcexf  30518  sbccom2  30530  sbccom2f  30531  sbccom2fi  30532  csbcom2fi  30534  prtlem70  30592  prtlem16  30610  fz1eqin  30702  7rexfrabdioph  30733  rmydioph  30956  dford4  30971  areaquad  31184  undisjrab  31186  isprm7  31192  pm13.196a  31321  fourierdlem42  31931  2reu7  32196  2reu8  32197  dfdfat2  32216  aovov0bi  32281  usgra2pth0  32355  initoid  32611  termoid  32612  rabsssn  32920  opeliun2xp  32922  aacllem  33216  eelT11  33496  eelTT1  33502  eelT01  33503  eel0T1  33504  uunTT1  33590  uunTT1p1  33591  uunTT1p2  33592  uunT11  33593  uunT11p1  33594  uunT11p2  33595  uun111  33602  bnj250  33753  bnj334  33765  bnj345  33766  bnj89  33774  bnj115  33778  bnj919  33825  bnj1304  33878  bnj92  33920  bnj124  33929  bnj126  33931  bnj154  33936  bnj155  33937  bnj523  33945  bnj526  33946  bnj540  33950  bnj581  33966  bnj916  33991  bnj929  33994  bnj964  34001  bnj978  34007  bnj983  34009  bnj1039  34027  bnj1040  34028  bnj1123  34042  bnj1128  34046  bnj1398  34090  bj-nf2  34196  bj-sbeq  34468  bj-csbsnlem  34470  bj-elsngl  34526  bj-eltag  34535  bj-tagex  34545  bj-projun  34552  bj-eldiag  34606  bj-eldiag2  34607  ishlat2  35078  polval2N  35630  dicelval3  36907  mapdordlem1a  37361  bj-ifim123g  37706  bj-ifidg  37707  bj-ifid1g  37708  bj-ifimimb  37715  bj-if1bi  37720  bj-ifbibib  37721  bj-ifororb  37726  bj-ifan23  37729  bj-ifdfxor  37732  bj-ifdfnan  37734  rp-fakenanass  37739  rp-fakeuninass  37741  cllem0  37751  xpcogend  37773  cotr2g  37786  dfxor4  37789  rp-imass  37795  dfhe3  37799  frege72  37963
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