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

Theorem 3bitri 286
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 264 . 2 (𝜓𝜃)
51, 4bitri 264 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  bibi1i  327  pm5.32  555  an32  617  orbi1i  878  orass  886  or32  890  annotanannotOLD  990  cases  1027  an3andi  1592  an33rean  1593  nanbi  1601  excxor  1616  cadan  1695  cadcomb  1699  nic-axALT  1746  tbw-bijust  1770  rb-bijust  1821  nf2  1858  19.43  1961  19.43OLD  1962  3exdistr  2037  19.12vvv  2074  excom13  2199  19.12vv  2341  eeeanv  2344  ee4anv  2345  sbn  2537  sb3an  2546  sbnf2  2588  sbcom2  2592  sbel2x  2606  sbco4  2613  2sb8e  2614  mo2v  2624  sb8eu  2651  2mo2  2698  2eu7  2707  2eu8  2708  r19.23v  3170  r19.26-3  3213  ralcom13  3247  rexcom13  3248  cbvreu  3317  ceqsralt  3378  ceqsex2  3393  ceqsex4v  3396  ralrab2  3522  rexrab2  3524  reu2  3544  rmo4  3549  reu8  3552  2reu5lem3  3565  sbc3an  3643  reu8nf  3663  rmo2  3673  rmo3  3675  dfss2  3738  ss2rab  3825  rabss  3826  ssrab  3827  dfdif3  3869  dfss4  4005  undi  4021  undif3  4035  difin2  4036  dfnul2  4063  difin0ss  4091  disj  4158  disj4  4167  rabsssn  4351  disjsn  4381  raldifsni  4459  ssunpr  4496  sspr  4497  sstp  4498  uni0b  4597  uni0c  4598  ssint  4625  iunss  4693  iundif2  4719  disjor  4766  reusv2lem4  5000  nfnid  5025  ssextss  5050  eqvinop  5082  opcom  5092  opeqsnOLD  5096  opeqpr  5097  brabsb  5119  opelopabf  5133  dfid3  5158  pofun  5186  opeliunxp  5310  xpiundi  5313  brinxp2  5320  ssrelOLD  5348  reliun  5378  exopxfr  5404  cnvuni  5447  dmopab3  5475  opelresOLD  5544  elres  5576  elsnres  5577  restidsing  5599  asymref2  5654  intirr  5655  xpeq0  5695  xpdifid  5703  ssrnres  5713  dminxp  5715  dfrel4v  5725  dmsnn0  5741  rnco  5785  coeq0  5788  sspred  5831  wfi  5856  sb8iota  6001  dffun2  6041  fun11  6103  isarep1  6117  dff1o4  6286  opabiota  6403  fvopab5  6452  fvn0ssdmfun  6493  fnressn  6567  f13dfv  6672  dff1o6  6673  fliftel  6701  oprabid  6821  mpt22eqb  6915  ralrnmpt2  6921  uniuni  7117  dflim3  7193  dfom2  7213  elxp4  7256  elxp5  7257  opabex3d  7291  opabex3  7292  el2xptp  7359  xporderlem  7438  dfrecs3  7621  tz7.48lem  7688  seqomlem2  7698  oaord  7780  oeeu  7836  nnaord  7852  ecid  7963  mptelixpg  8098  elixpsn  8100  xpsnen  8199  xpcomco  8205  xpassen  8209  omxpenlem  8216  dom0  8243  modom  8316  tz9.12lem3  8815  rankxpsuc  8908  cp  8917  cardprclem  9004  infxpenlem  9035  dfac5lem1  9145  dfac5lem2  9146  dfac5lem5  9149  dfac10c  9161  kmlem3  9175  kmlem12  9184  kmlem13  9185  kmlem14  9186  kmlem15  9187  ackbij2  9266  cflim2  9286  dffin7-2  9421  dfacfin7  9422  fin1a2lem12  9434  axdc3lem3  9475  cfpwsdom  9607  recmulnq  9987  genpass  10032  psslinpr  10054  suplem2pr  10076  opelreal  10152  ltxrlt  10309  addid1  10417  fimaxre  11169  elnn0  11495  elxnn0  11566  elnn0z  11591  nnwos  11957  elxr  12154  xrnepnf  12156  elfzuzb  12542  4fvwrd4  12666  preduz  12668  elfzo2  12680  ssnn0fi  12991  sqeqori  13182  xpcogend  13922  cotr2g  13924  fsumcom2  14712  modfsummod  14732  fprodcom2  14920  rpnnen2lem12  15159  gcdcllem1  15428  isprm2  15601  isprm7  15626  pythagtriplem2  15728  infpn2  15823  4sqlem12  15866  initoid  16861  termoid  16862  eldmcoa  16921  oduposb  17343  gsumwspan  17590  isnsg2  17831  isnsg4  17844  efgcpbllemb  18374  dmdprd  18604  dprdval  18609  dprdw  18616  dprd2d2  18650  dfrhm2  18926  brric2  18954  issubrg  18989  islmim  19274  lbsextlem2  19373  opsrtoslem1  19698  cnfldfunALT  19973  pjfval2  20269  fvmptnn04if  20873  ntreq0  21101  cmpcov2  21413  cmpsub  21423  2ndcdisj  21479  unisngl  21550  txbas  21590  elpt  21595  txkgen  21675  xkococn  21683  fbun  21863  trfil2  21910  fin1aufil  21955  alexsubALTlem3  22072  cnextcn  22090  qustgplem  22143  eltsms  22155  ustn0  22243  fmucndlem  22314  metrest  22548  restmetu  22594  isclmp  23115  srabn  23374  ellogdm  24605  1cubr  24789  leibpilem2  24888  dmarea  24904  vmasum  25161  dchrelbas2  25182  2lgslem4  25351  tgcgr4  25646  ltgov  25712  axlowdimlem13  26054  axeuclidlem  26062  numedglnl  26260  nbgrelOLD  26456  nbupgrres  26487  vtxd0nedgb  26618  rusgrprc  26720  usgr2pth0  26895  wspthsnwspthsnon  27058  isclwwlk  27131  clwwlkn1  27194  clwwlkn2  27197  clwwlknonel  27266  3pthdlem1  27341  iseupthf1o  27379  frgr3v  27454  fusgr2wsp2nb  27513  frgrregord013  27588  h2hcau  28170  h2hlm  28171  axhcompl-zf  28189  shlesb1i  28579  shne0i  28641  chnlei  28678  cmbr2i  28789  pjneli  28916  ho02i  29022  adjsym  29026  adjeu  29082  lnopeqi  29201  largei  29460  atoml2i  29576  cdj3lem3b  29633  or3di  29641  mo5f  29658  rmo3f  29668  rmo4fOLD  29669  disjnf  29716  disjorf  29724  ssrelf  29759  ofpreima  29799  disjdsct  29814  1stpreima  29818  2ndpreima  29819  f1od2  29833  xrdifh  29876  nndiffz1  29882  ordtconnlem1  30304  ind1a  30415  measiuns  30614  elunirnmbfm  30649  eulerpartlemr  30770  eulerpartlemgh  30774  eulerpartlemn  30777  ballotlemodife  30893  bnj250  31101  bnj334  31113  bnj345  31114  bnj89  31121  bnj115  31125  bnj919  31169  bnj1304  31222  bnj92  31264  bnj124  31273  bnj126  31275  bnj154  31280  bnj155  31281  bnj523  31289  bnj526  31290  bnj540  31294  bnj581  31310  bnj916  31335  bnj929  31338  bnj964  31345  bnj978  31351  bnj983  31353  bnj1039  31371  bnj1040  31372  bnj1123  31386  bnj1128  31390  bnj1398  31434  cvmlift2lem1  31616  elmthm  31805  quad3  31896  3orit  31928  brtp  31971  dftr6  31972  dfpo2  31977  eldm3  31983  elrn3  31984  elima4  32009  19.12b  32037  frpoind  32071  frind  32074  nosupbnd1lem4  32188  nosupbnd2lem1  32192  slenlt  32208  madeval2  32267  brtxp  32318  brtxp2  32319  brpprod  32323  brpprod3a  32324  elfix  32341  dffix2  32343  ellimits  32348  dffun10  32352  elfuns  32353  elsingles  32356  brimg  32375  brapply  32376  brsuccf  32379  funpartlem  32380  brrestrict  32387  dfrecs2  32388  dfrdg4  32389  brlb  32393  altopthc  32409  altopthd  32410  fvtransport  32470  hfext  32621  nn0prpw  32649  filnetlem4  32707  df3nandALT2  32728  bj-ssbn  32972  bj-cleljustab  33175  bj-sbeq  33219  bj-csbsnlem  33221  bj-elsngl  33281  bj-eltag  33290  bj-tagex  33300  bj-projun  33307  bj-disj2r  33338  bj-restuni  33375  bj-eldiag  33421  bj-eldiag2  33422  topdifinffinlem  33525  relowlpssretop  33542  phpreu  33719  poimirlem24  33759  poimirlem26  33761  poimirlem30  33765  areacirclem5  33829  isbnd2  33907  sbcalf  34242  sbcexf  34243  sbccom2  34255  sbccom2f  34256  sbccom2fi  34257  csbcom2fi  34259  anan  34337  brinxp2ALTV  34370  idinxpssinxp2  34425  ineleq  34454  brabidga  34463  inxpxrn  34488  rnxrn  34491  cossssid2  34553  cossssid3  34554  cosscnvssid3  34561  prtlem70  34657  prtlem16  34670  ishlat2  35155  polval2N  35707  dicelval3  36983  mapdordlem1a  37437  fz1eqin  37851  7rexfrabdioph  37883  rmydioph  38100  dford4  38115  areaquad  38321  ifpan23  38323  ifpdfnan  38350  ifpdfxor  38351  ifpidg  38355  ifpid1g  38358  ifpim123g  38364  ifp1bi  38366  ifpimimb  38368  ifpororb  38369  ifpbibib  38374  rp-fakenanass  38379  rp-fakeuninass  38381  cllem0  38390  rababg  38398  elmapintrab  38401  elmapintab  38421  undmrnresiss  38429  ss2iundf  38470  dfxor4  38577  rp-imass  38584  dfhe3  38588  dffrege115  38791  frege131  38807  frege133  38809  clsk1indlem4  38861  clsk1indlem1  38862  undisjrab  39024  pm13.196a  39134  eelT11  39451  eelTT1  39454  eelT01  39455  eel0T1  39456  uunTT1  39539  uunTT1p1  39540  uunTT1p2  39541  uunT11  39542  uunT11p1  39543  uunT11p2  39544  uun111  39551  iunssf  39778  ssrabf  39813  rabssf  39817  disjinfi  39894  elicores  40272  fourierdlem42  40877  iundjiun  41188  2reu7  41705  2reu8  41706  dfdfat2  41725  aovov0bi  41790  257prm  41991  fmtno4prmfac  42002  nnsum4primeseven  42206  nnsum4primesevenALTV  42207  uspgrsprf1  42273  opeliun2xp  42629  aacllem  43068
  Copyright terms: Public domain W3C validator