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  orbi1i  541  orass  545  or32  548  pm5.32  669  an32  856  annotanannotOLD  960  cases  1011  an3andi  1485  an33rean  1486  nanbi  1494  excxor  1509  cadan  1588  cadcomb  1592  nic-axALT  1639  tbw-bijust  1663  rb-bijust  1714  nf2  1751  19.43  1850  19.43OLD  1851  3exdistr  1926  19.12vvv  1963  excom13  2084  19.12vv  2216  eeeanv  2219  ee4anv  2220  sbn  2419  sb3an  2428  sbnf2  2467  sbcom2  2473  sbel2x  2487  sbco4  2494  2sb8e  2495  mo2v  2505  sb8eu  2532  2mo2  2579  2eu7  2588  2eu8  2589  r19.23v  3052  r19.26-3  3095  ralcom13  3129  rexcom13  3130  cbvreu  3199  ceqsralt  3260  ceqsex2  3275  ceqsex4v  3278  ralrab2  3405  rexrab2  3407  reu2  3427  rmo4  3432  reu8  3435  2reu5lem3  3448  sbc3an  3527  reu8nf  3549  rmo2  3559  rmo3  3561  dfss2  3624  ss2rab  3711  rabss  3712  ssrab  3713  dfss4  3891  undi  3907  undif3  3921  undif3OLD  3922  difin2  3923  dfnul2  3950  difin0ss  3979  disj  4050  disj4  4058  rabsssn  4247  disjsn  4278  raldifsni  4357  ssunpr  4397  sspr  4398  sstp  4399  uni0b  4495  uni0c  4496  ssint  4525  iunss  4593  iundif2  4619  disjor  4666  reusv2lem4  4902  nfnid  4927  ssextss  4952  eqvinop  4984  opcom  4994  opeqsn  4996  opeqpr  4997  brabsb  5015  opelopabf  5029  dfid3  5054  pofun  5080  opeliunxp  5204  xpiundi  5207  brinxp2  5214  ssrelOLD  5242  reliun  5272  exopxfr  5298  cnvuni  5341  dmopab3  5369  opelresOLD  5438  elres  5470  elsnres  5471  restidsing  5493  asymref2  5548  intirr  5549  xpeq0  5589  xpdifid  5597  ssrnres  5607  dminxp  5609  dfrel4v  5619  dmsnn0  5635  rnco  5679  coeq0  5682  sspred  5726  wfi  5751  sb8iota  5896  dffun2  5936  fun11  6001  isarep1  6015  dff1o4  6183  opabiota  6300  fvopab5  6349  fvn0ssdmfun  6390  fnressn  6465  f13dfv  6570  dff1o6  6571  fliftel  6599  oprabid  6717  mpt22eqb  6811  ralrnmpt2  6817  uniuni  7013  dflim3  7089  dfom2  7109  elxp4  7152  elxp5  7153  opabex3d  7187  opabex3  7188  el2xptp  7255  xporderlem  7333  dfrecs3  7514  tz7.48lem  7581  seqomlem2  7591  oaord  7672  oeeu  7728  nnaord  7744  ecid  7855  mptelixpg  7987  elixpsn  7989  mapsnen  8076  xpsnen  8085  xpcomco  8091  xpassen  8095  omxpenlem  8102  dom0  8129  modom  8202  tz9.12lem3  8690  rankxpsuc  8783  cp  8792  cardprclem  8843  infxpenlem  8874  dfac5lem1  8984  dfac5lem2  8985  dfac5lem5  8988  dfac10c  8998  kmlem3  9012  kmlem12  9021  kmlem13  9022  kmlem14  9023  kmlem15  9024  ackbij2  9103  cflim2  9123  dffin7-2  9258  dfacfin7  9259  fin1a2lem12  9271  axdc3lem3  9312  cfpwsdom  9444  recmulnq  9824  genpass  9869  psslinpr  9891  suplem2pr  9913  opelreal  9989  ltxrlt  10146  addid1  10254  fimaxre  11006  elnn0  11332  elxnn0  11403  elnn0z  11428  nnwos  11793  elxr  11988  xrnepnf  11990  elfzuzb  12374  4fvwrd4  12498  preduz  12500  elfzo2  12512  ssnn0fi  12824  sqeqori  13016  xpcogend  13759  cotr2g  13761  fsumcom2  14549  fsumcom2OLD  14550  modfsummod  14570  fprodcom2  14758  fprodcom2OLD  14759  rpnnen2lem12  14998  gcdcllem1  15268  isprm2  15442  isprm7  15467  pythagtriplem2  15569  infpn2  15664  4sqlem12  15707  initoid  16702  termoid  16703  eldmcoa  16762  oduposb  17183  gsumwspan  17430  isnsg2  17671  isnsg4  17684  efgcpbllemb  18214  dmdprd  18443  dprdval  18448  dprdw  18455  dprd2d2  18489  dfrhm2  18765  brric2  18793  issubrg  18828  islmim  19110  lbsextlem2  19207  opsrtoslem1  19532  cnfldfunALT  19807  pjfval2  20101  fvmptnn04if  20702  ntreq0  20929  cmpcov2  21241  cmpsub  21251  2ndcdisj  21307  unisngl  21378  txbas  21418  elpt  21423  txkgen  21503  xkococn  21511  fbun  21691  trfil2  21738  fin1aufil  21783  alexsubALTlem3  21900  cnextcn  21918  qustgplem  21971  eltsms  21983  ustn0  22071  fmucndlem  22142  metrest  22376  restmetu  22422  isclmp  22943  srabn  23202  ellogdm  24430  1cubr  24614  leibpilem2  24713  dmarea  24729  vmasum  24986  dchrelbas2  25007  2lgslem4  25176  tgcgr4  25471  ltgov  25537  axlowdimlem13  25879  axeuclidlem  25887  numedglnl  26084  nbgrelOLD  26279  nbupgrres  26310  vtxd0nedgb  26440  rusgrprc  26542  usgr2pth0  26717  wspthsnwspthsnon  26879  isclwwlk  26952  clwwlkn1  27004  clwwlkn2  27007  clwwlknonel  27070  3pthdlem1  27142  iseupthf1o  27180  frgr3v  27255  fusgr2wsp2nb  27314  frgrregord013  27382  h2hcau  27964  h2hlm  27965  axhcompl-zf  27983  shlesb1i  28373  shne0i  28435  chnlei  28472  cmbr2i  28583  pjneli  28710  ho02i  28816  adjsym  28820  adjeu  28876  lnopeqi  28995  largei  29254  atoml2i  29370  cdj3lem3b  29427  or3di  29435  mo5f  29452  rmo3f  29462  rmo4fOLD  29463  disjnf  29510  disjorf  29518  ssrelf  29553  ofpreima  29593  disjdsct  29608  1stpreima  29612  2ndpreima  29613  f1od2  29627  xrdifh  29670  nndiffz1  29676  ordtconnlem1  30098  ind1a  30209  measiuns  30408  elunirnmbfm  30443  eulerpartlemr  30564  eulerpartlemgh  30568  eulerpartlemn  30571  ballotlemodife  30687  bnj250  30895  bnj334  30907  bnj345  30908  bnj89  30915  bnj115  30919  bnj919  30963  bnj1304  31016  bnj92  31058  bnj124  31067  bnj126  31069  bnj154  31074  bnj155  31075  bnj523  31083  bnj526  31084  bnj540  31088  bnj581  31104  bnj916  31129  bnj929  31132  bnj964  31139  bnj978  31145  bnj983  31147  bnj1039  31165  bnj1040  31166  bnj1123  31180  bnj1128  31184  bnj1398  31228  cvmlift2lem1  31410  elmthm  31599  quad3  31690  3orit  31722  brtp  31765  dftr6  31766  dfpo2  31771  eldm3  31777  elrn3  31778  elima4  31803  19.12b  31831  frpoind  31865  frind  31868  nosupbnd1lem4  31982  nosupbnd2lem1  31986  slenlt  32002  madeval2  32061  brtxp  32112  brtxp2  32113  brpprod  32117  brpprod3a  32118  elfix  32135  dffix2  32137  ellimits  32142  dffun10  32146  elfuns  32147  elsingles  32150  brimg  32169  brapply  32170  brsuccf  32173  funpartlem  32174  brrestrict  32181  dfrecs2  32182  dfrdg4  32183  brlb  32187  altopthc  32203  altopthd  32204  fvtransport  32264  hfext  32415  nn0prpw  32443  filnetlem4  32501  df3nandALT2  32522  bj-ssbn  32766  bj-cleljustab  32972  bj-sbeq  33021  bj-csbsnlem  33023  bj-elsngl  33081  bj-eltag  33090  bj-tagex  33100  bj-projun  33107  bj-disj2r  33138  bj-restuni  33175  bj-eldiag  33221  bj-eldiag2  33222  topdifinffinlem  33325  relowlpssretop  33342  phpreu  33523  poimirlem24  33563  poimirlem26  33565  poimirlem30  33569  areacirclem5  33634  isbnd2  33712  sbcalf  34047  sbcexf  34048  sbccom2  34060  sbccom2f  34061  sbccom2fi  34062  csbcom2fi  34064  anan  34142  brinxp2ALTV  34175  idinxpssinxp2  34230  ineleq  34259  brabidga  34268  inxpxrn  34293  rnxrn  34296  cossssid2  34358  cossssid3  34359  cosscnvssid3  34366  prtlem70  34460  prtlem16  34473  ishlat2  34958  polval2N  35510  dicelval3  36786  mapdordlem1a  37240  fz1eqin  37649  7rexfrabdioph  37681  rmydioph  37898  dford4  37913  areaquad  38119  ifpan23  38121  ifpdfnan  38148  ifpdfxor  38149  ifpidg  38153  ifpid1g  38156  ifpim123g  38162  ifp1bi  38164  ifpimimb  38166  ifpororb  38167  ifpbibib  38172  rp-fakenanass  38177  rp-fakeuninass  38179  cllem0  38188  rababg  38196  elmapintrab  38199  elmapintab  38219  undmrnresiss  38227  ss2iundf  38268  dfxor4  38375  rp-imass  38382  dfhe3  38386  dffrege115  38589  frege131  38605  frege133  38607  clsk1indlem4  38659  clsk1indlem1  38660  undisjrab  38822  pm13.196a  38932  eelT11  39249  eelTT1  39252  eelT01  39253  eel0T1  39254  uunTT1  39337  uunTT1p1  39338  uunTT1p2  39339  uunT11  39340  uunT11p1  39341  uunT11p2  39342  uun111  39349  iunssf  39577  ssrabf  39612  rabssf  39616  disjinfi  39694  elicores  40078  fourierdlem42  40684  iundjiun  40995  2reu7  41512  2reu8  41513  dfdfat2  41532  aovov0bi  41597  257prm  41798  fmtno4prmfac  41809  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  uspgrsprf1  42080  opeliun2xp  42436  aacllem  42875
  Copyright terms: Public domain W3C validator