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

Theorem 3bitri 300
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 278 . 2 (𝜓𝜃)
51, 4bitri 278 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 209
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 210
This theorem is referenced by:  bibi1i  342  pm5.32  577  biadan  818  orbi1i  911  orass  919  or32  923  cases  1038  3anidm  1101  an3andi  1479  an33rean  1480  an33reanOLD  1481  nanbi  1491  excxor  1508  norassOLD  1535  cadan  1611  cadcomb  1615  nic-axALT  1676  tbw-bijust  1700  rb-bijust  1751  nf2  1787  19.43  1883  19.43OLD  1884  3exdistr  1962  19.12vvv  1995  sb3an  2086  equsb3rOLD  2108  sbcom2  2165  excom13  2168  sbco4  2280  sbn  2283  19.12vv  2357  eeeanv  2360  ee4anv  2361  2sb8ev  2364  sbel2x  2487  2sb8e  2552  sbnALT  2571  dfmo  2657  sb8eulem  2659  2mo2  2709  2eu7  2720  2eu8  2721  r19.26-3  3139  r19.23v  3238  rexcom  3308  ralcom13  3312  rexcom13  3313  cbvreuw  3389  cbvreu  3394  ceqsralt  3475  ceqsex2  3491  ceqsex2v  3492  ceqsex4v  3494  ralrab2  3638  rexrab2  3641  reu2  3664  rmo4  3669  reu8  3672  rmo3f  3673  2reu5lem3  3696  sbc3an  3785  reu8nf  3806  rmo2  3816  rmo3  3818  rmoanim  3823  dfss2OLD  3902  ss2rab  3998  rabss  3999  ssrab  4000  dfdif3  4042  symdifass  4178  dfss4  4185  undi  4201  undif3  4215  difin2  4216  difin0ss  4282  disj  4355  disjOLD  4356  disj4  4366  rabsssn  4567  disjsn  4607  raldifsni  4688  ssunpr  4725  sspr  4726  sstp  4727  uni0b  4826  uni0c  4827  ssint  4854  iunssf  4931  iunss  4932  iundif2  4959  disjor  5010  nfnid  5241  reusv2lem4  5267  ssextss  5311  exss  5320  eqvinop  5343  sbcop  5345  opcom  5356  opeqpr  5360  brabsb  5383  opelopabf  5397  dfid3  5427  pofun  5455  opeliunxp  5583  xpiundi  5586  brinxp2  5593  reliun  5653  exopxfr  5678  cnvuni  5721  dmopab3  5752  rnep  5761  elres  5857  elsnres  5858  elrid  5880  asymref2  5944  intirr  5945  xpeq0  5984  xpdifid  5992  ssrnres  6002  dminxp  6004  dfrel4v  6014  elid  6023  dmsnn0  6031  rnco  6072  coeq0  6075  resssxp  6089  sspred  6124  wfi  6149  sb8iota  6294  dffun2  6334  fun11  6398  isarep1  6412  dff1o4  6598  opabiota  6721  fvopab5  6777  eqfnfv3  6781  fvn0ssdmfun  6819  fnressn  6897  f13dfv  7009  dff1o6  7010  fliftel  7041  oprabidw  7166  oprabid  7167  mpo2eqb  7262  ralrnmpo  7268  uniuni  7464  dflim3  7542  dfom2  7562  elxp4  7609  elxp5  7610  opabex3d  7648  opabex3rd  7649  opabex3  7650  el2xptp  7717  fsplit  7795  xporderlem  7804  dfrecs3  7992  tz7.48lem  8060  seqomlem2  8070  oaord  8156  oeeu  8212  nnaord  8228  ecid  8345  mptelixpg  8482  elixpsn  8484  xpsnen  8584  xpcomco  8590  xpassen  8594  omxpenlem  8601  dom0  8629  modom  8703  tz9.12lem3  9202  rankxpsuc  9295  cp  9304  cardprclem  9392  infxpenlem  9424  dfac5lem1  9534  dfac5lem2  9535  dfac5lem5  9538  dfac10c  9549  kmlem3  9563  kmlem12  9572  kmlem13  9573  kmlem14  9574  kmlem15  9575  ackbij2  9654  cf0  9662  cflim2  9674  dffin7-2  9809  dfacfin7  9810  fin1a2lem12  9822  axdc3lem3  9863  cfpwsdom  9995  recmulnq  10375  genpass  10420  psslinpr  10442  suplem2pr  10464  opelreal  10541  ltxrlt  10700  addid1  10809  elnn0  11887  elxnn0  11957  elnn0z  11982  nnwos  12303  elxr  12499  xrnepnf  12501  elfzuzb  12896  4fvwrd4  13022  preduz  13024  elfzo2  13036  ssnn0fi  13348  sqeqori  13572  xpcogend  14325  cotr2g  14327  fsumcom2  15121  modfsummod  15141  fprodcom2  15330  rpnnen2lem12  15570  gcdcllem1  15838  isprm2  16016  isprm7  16042  pythagtriplem2  16144  infpn2  16239  4sqlem12  16282  initoid  17257  termoid  17258  eldmcoa  17317  oduposb  17738  gsumwspan  18003  smndex1basss  18062  smndex1mgm  18064  isnsg2  18300  isnsg4  18311  cycsubmel  18335  efgcpbllemb  18873  dmdprd  19113  dprdval  19118  dprdw  19125  dprd2d2  19159  dfrhm2  19465  brric2  19493  issubrg  19528  islmim  19827  lbsextlem2  19924  cnfldfunALT  20104  pjfval2  20398  opsrtoslem1  20723  ntreq0  21682  cmpcov2  21995  cmpsub  22005  2ndcdisj  22061  unisngl  22132  txbas  22172  elpt  22177  txkgen  22257  xkococn  22265  fbun  22445  trfil2  22492  fin1aufil  22537  alexsubALTlem3  22654  cnextcn  22672  qustgplem  22726  eltsms  22738  ustn0  22826  fmucndlem  22897  metrest  23131  restmetu  23177  isclmp  23702  srabn  23964  ellogdm  25230  1cubr  25428  leibpilem2  25527  dmarea  25543  vmasum  25800  dchrelbas2  25821  2lgslem4  25990  tgcgr4  26325  ltgov  26391  axlowdimlem13  26748  axeuclidlem  26756  numedglnl  26937  nbupgrres  27154  vtxd0nedgb  27278  rusgrprc  27380  usgr2pth0  27554  wspthsnwspthsnon  27702  isclwwlk  27769  clwwlkn1  27826  clwwlkn2  27829  clwwlknonel  27880  3pthdlem1  27949  iseupthf1o  27987  frgr3v  28060  fusgr2wsp2nb  28119  frgrregord013  28180  h2hcau  28762  h2hlm  28763  shlesb1i  29169  shne0i  29231  chnlei  29268  cmbr2i  29379  pjneli  29506  ho02i  29612  adjsym  29616  adjeu  29672  lnopeqi  29791  largei  30050  atoml2i  30166  cdj3lem3b  30223  or3di  30231  mo5f  30260  dmrab  30267  disjnf  30333  disjorf  30342  ssrelf  30379  ofpreima  30428  disjdsct  30462  1stpreima  30466  2ndpreima  30467  f1od2  30483  xrdifh  30529  nndiffz1  30535  prmidl0  31034  zarclsun  31223  ordtconnlem1  31277  ind1a  31388  measiuns  31586  elunirnmbfm  31621  eulerpartlemr  31742  eulerpartlemgh  31746  eulerpartlemn  31749  ballotlemodife  31865  bnj250  32081  bnj334  32093  bnj345  32094  bnj89  32101  bnj115  32105  bnj919  32148  bnj1304  32201  bnj92  32244  bnj124  32253  bnj126  32255  bnj154  32260  bnj155  32261  bnj523  32269  bnj526  32270  bnj540  32274  bnj581  32290  bnj916  32315  bnj929  32318  bnj964  32325  bnj978  32331  bnj983  32333  bnj1039  32353  bnj1040  32354  bnj1123  32368  bnj1128  32372  bnj1398  32416  lfuhgr3  32479  cvmlift2lem1  32662  satfv0  32718  satf0  32732  satf0op  32737  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  elmthm  32936  quad3  33026  3orit  33058  brtp  33098  dftr6  33099  dfpo2  33104  eldm3  33110  elrn3  33111  elima4  33132  19.12b  33159  frpoind  33193  frind  33198  nosupbnd1lem4  33324  nosupbnd2lem1  33328  slenlt  33344  madeval2  33403  brtxp  33454  brtxp2  33455  brpprod  33459  brpprod3a  33460  elfix  33477  dffix2  33479  ellimits  33484  sscoid  33487  dffun10  33488  elfuns  33489  elsingles  33492  brimg  33511  brapply  33512  brsuccf  33515  funpartlem  33516  brrestrict  33523  dfrecs2  33524  dfrdg4  33525  brlb  33529  altopthc  33545  altopthd  33546  fvtransport  33606  hfext  33757  nn0prpw  33784  filnetlem4  33842  df3nandALT2  33861  bj-sbeq  34342  bj-csbsnlem  34344  bj-elsngl  34404  bj-eltag  34413  bj-tagex  34423  bj-projun  34430  bj-reabeq  34463  bj-disj2r  34464  bj-restuni  34512  bj-elid6  34585  bj-eldiag  34591  bj-eldiag2  34592  topdifinffinlem  34764  relowlpssretop  34781  fvineqsneq  34829  wl-3xorbi  34890  wl-2mintru1  34907  wl-df3maxtru1  34909  wl-dfclab  34993  wl-dfrexsb  35016  phpreu  35041  poimirlem24  35081  poimirlem26  35083  poimirlem30  35087  areacirclem5  35149  isbnd2  35221  sbcalf  35552  sbcexf  35553  sbccom2  35563  sbccom2f  35564  sbccom2fi  35565  csbcom2fi  35566  anan  35659  idinxpssinxp2  35735  ineleq  35768  brabidgaw  35777  brabidga  35778  inxpxrn  35803  rnxrn  35806  cossssid2  35868  cossssid3  35869  cosscnvssid3  35876  dfeldisj3  36112  dfeldisj4  36113  prtlem70  36153  prtlem16  36165  ishlat2  36649  pmapglb  37066  polval2N  37202  dicelval3  38476  mapdordlem1a  38930  prjspeclsp  39604  fz1eqin  39708  7rexfrabdioph  39739  rmydioph  39953  dford4  39968  areaquad  40164  ifpan23  40166  ifpdfnan  40192  ifpdfxor  40193  ifpidg  40197  ifpid1g  40200  ifpim123g  40206  ifp1bi  40208  ifpimimb  40210  ifpororb  40211  ifpbibib  40216  rp-fakeuninass  40222  dfsucon  40229  cllem0  40263  rababg  40271  elmapintrab  40274  elmapintab  40294  undmrnresiss  40302  ss2iundf  40358  dfxor4  40465  dfhe3  40474  dffrege115  40677  frege131  40693  frege133  40695  clsk1indlem4  40745  clsk1indlem1  40746  expandrexn  40997  rr-groth  41005  undisjrab  41008  pm13.196a  41116  eelT11  41411  eelTT1  41414  eelT01  41415  eel0T1  41416  uunTT1  41497  uunTT1p1  41498  uunTT1p2  41499  uunT11  41500  uunT11p1  41501  uunT11p2  41502  uun111  41509  ssrabf  41748  rabssf  41752  disjinfi  41818  elicores  42168  fourierdlem42  42789  iundjiun  43097  2reu7  43665  2reu8  43666  2reu8i  43667  dfdfat2  43682  aovov0bi  43750  afv2orxorb  43782  afv2ndeffv0  43814  ichcircshi  43969  ichan  43970  icheq  43977  ichal  43981  prpair  44016  prproropf1olem0  44017  257prm  44076  fmtno4prmfac  44087  nnsum4primeseven  44316  nnsum4primesevenALTV  44317  uspgrsprf1  44373  opeliun2xp  44732  rrx2xpref1o  45130  aacllem  45327
  Copyright terms: Public domain W3C validator