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  328  orbi1i  542  orass  546  or32  549  pm5.32  667  an32  838  cases  991  an3andi  1443  an33rean  1444  nanbi  1452  excxor  1467  cadan  1546  cadcomb  1550  nic-axALT  1597  tbw-bijust  1621  rb-bijust  1672  nf2  1709  19.43  1808  19.43OLD  1809  19.12vvv  1905  3exdistr  1921  excom13  2042  19.12vv  2178  eeeanv  2181  ee4anv  2182  sbn  2389  sb3an  2398  sbnf2  2437  sbcom2  2443  sbel2x  2457  sbco4  2464  2sb8e  2465  mo2v  2475  sb8eu  2501  2mo2  2548  2eu7  2557  2eu8  2558  r19.23v  3019  r19.26-3  3062  ralcom13  3095  rexcom13  3096  cbvreu  3164  ceqsralt  3224  ceqsex2  3239  ceqsex4v  3242  ralrab2  3366  rexrab2  3368  reu2  3388  rmo4  3393  reu8  3396  2reu5lem3  3409  sbc3an  3488  rmo2  3519  rmo3  3521  dfss2  3584  ss2rab  3670  rabss  3671  ssrab  3672  dfss4  3850  undi  3866  undif3  3880  undif3OLD  3881  difin2  3882  dfnul2  3909  difin0ss  3937  disj  4008  disj4  4016  rabsssn  4206  disjsn  4237  raldifsni  4315  ssunpr  4356  sspr  4357  sstp  4358  uni0b  4454  uni0c  4455  ssint  4484  iunss  4552  iundif2  4578  disjor  4625  reusv2lem4  4863  nfnid  4888  ssextss  4913  eqvinop  4945  opcom  4955  opeqsn  4957  opeqpr  4958  brabsb  4976  opelopabf  4990  dfid3  5015  pofun  5041  opeliunxp  5160  xpiundi  5163  brinxp2  5170  ssrelOLD  5198  reliun  5229  exopxfr  5254  cnvuni  5298  dmopab3  5326  opelres  5390  elres  5423  elsnres  5424  restidsing  5446  asymref2  5501  intirr  5502  xpeq0  5542  xpdifid  5550  ssrnres  5560  dminxp  5562  dfrel4v  5572  dmsnn0  5588  rnco  5629  coeq0  5632  sspred  5676  wfi  5701  sb8iota  5846  dffun2  5886  fun11  5951  isarep1  5965  dff1o4  6132  opabiota  6248  fvopab5  6295  fvn0ssdmfun  6336  fnressn  6410  f13dfv  6515  dff1o6  6516  fliftel  6544  oprabid  6662  mpt22eqb  6754  ralrnmpt2  6760  uniuni  6956  dflim3  7032  dfom2  7052  elxp4  7095  elxp5  7096  opabex3d  7130  opabex3  7131  el2xptp  7196  xporderlem  7273  dfrecs3  7454  tz7.48lem  7521  seqomlem2  7531  oaord  7612  oeeu  7668  nnaord  7684  ecid  7797  mptelixpg  7930  elixpsn  7932  mapsnen  8020  xpsnen  8029  xpcomco  8035  xpassen  8039  omxpenlem  8046  dom0  8073  modom  8146  tz9.12lem3  8637  rankxpsuc  8730  cp  8739  cardprclem  8790  infxpenlem  8821  dfac5lem1  8931  dfac5lem2  8932  dfac5lem5  8935  dfac10c  8945  kmlem3  8959  kmlem12  8968  kmlem13  8969  kmlem14  8970  kmlem15  8971  ackbij2  9050  cflim2  9070  dffin7-2  9205  dfacfin7  9206  fin1a2lem12  9218  axdc3lem3  9259  cfpwsdom  9391  recmulnq  9771  genpass  9816  psslinpr  9838  suplem2pr  9860  opelreal  9936  ltxrlt  10093  addid1  10201  fimaxre  10953  elnn0  11279  elxnn0  11350  elnn0z  11375  nnwos  11740  elxr  11935  xrnepnf  11937  elfzuzb  12321  4fvwrd4  12443  preduz  12445  elfzo2  12457  ssnn0fi  12767  sqeqori  12959  xpcogend  13694  cotr2g  13696  fsumcom2  14486  fsumcom2OLD  14487  modfsummod  14507  fprodcom2  14695  fprodcom2OLD  14696  rpnnen2lem12  14935  gcdcllem1  15202  isprm2  15376  isprm7  15401  pythagtriplem2  15503  infpn2  15598  4sqlem12  15641  initoid  16636  termoid  16637  eldmcoa  16696  oduposb  17117  gsumwspan  17364  isnsg2  17605  isnsg4  17618  efgcpbllemb  18149  dmdprd  18378  dprdval  18383  dprdw  18390  dprd2d2  18424  dfrhm2  18698  brric2  18726  issubrg  18761  islmim  19043  lbsextlem2  19140  opsrtoslem1  19465  cnfldfunALT  19740  pjfval2  20034  fvmptnn04if  20635  ntreq0  20862  cmpcov2  21174  cmpsub  21184  2ndcdisj  21240  unisngl  21311  txbas  21351  elpt  21356  txkgen  21436  xkococn  21444  fbun  21625  trfil2  21672  fin1aufil  21717  alexsubALTlem3  21834  cnextcn  21852  qustgplem  21905  eltsms  21917  ustn0  22005  fmucndlem  22076  metrest  22310  restmetu  22356  isclmp  22878  srabn  23137  ellogdm  24366  1cubr  24550  leibpilem2  24649  dmarea  24665  vmasum  24922  dchrelbas2  24943  2lgslem4  25112  tgcgr4  25407  ltgov  25473  axlowdimlem13  25815  axeuclidlem  25823  numedglnl  26020  nbgrel  26219  nbupgrres  26247  vtxd0nedgb  26365  rusgrprc  26467  usgr2pth0  26642  isclwwlks  26861  clwwlksn2  26890  3pthdlem1  27004  iseupthf1o  27042  frgr3v  27119  fusgr2wsp2nb  27172  frgrregord013  27223  h2hcau  27806  h2hlm  27807  axhcompl-zf  27825  shlesb1i  28215  shne0i  28277  chnlei  28314  cmbr2i  28425  pjneli  28552  ho02i  28658  adjsym  28662  adjeu  28718  lnopeqi  28837  largei  29096  atoml2i  29212  cdj3lem3b  29269  or3di  29277  mo5f  29296  rmo3f  29307  rmo4fOLD  29308  disjnf  29356  disjorf  29364  ssrelf  29397  ofpreima  29439  disjdsct  29454  1stpreima  29458  2ndpreima  29459  f1od2  29473  xrdifh  29516  nndiffz1  29522  ordtconnlem1  29944  ind1a  30055  measiuns  30254  elunirnmbfm  30289  eulerpartlemr  30410  eulerpartlemgh  30414  eulerpartlemn  30417  ballotlemodife  30533  bnj250  30741  bnj334  30753  bnj345  30754  bnj89  30761  bnj115  30765  bnj919  30811  bnj1304  30864  bnj92  30906  bnj124  30915  bnj126  30917  bnj154  30922  bnj155  30923  bnj523  30931  bnj526  30932  bnj540  30936  bnj581  30952  bnj916  30977  bnj929  30980  bnj964  30987  bnj978  30993  bnj983  30995  bnj1039  31013  bnj1040  31014  bnj1123  31028  bnj1128  31032  bnj1398  31076  cvmlift2lem1  31258  elmthm  31447  quad3  31538  3orit  31571  brtp  31614  dftr6  31615  dfpo2  31620  eldm3  31627  elrn3  31628  elima4  31653  19.12b  31681  frind  31714  nosupbnd1lem4  31831  nosupbnd2lem1  31835  slenlt  31851  madeval2  31910  brtxp  31962  brtxp2  31963  brpprod  31967  brpprod3a  31968  elfix  31985  dffix2  31987  ellimits  31992  dffun10  31996  elfuns  31997  elsingles  32000  brimg  32019  brapply  32020  brsuccf  32023  funpartlem  32024  brrestrict  32031  dfrecs2  32032  dfrdg4  32033  brlb  32037  altopthc  32053  altopthd  32054  fvtransport  32114  hfext  32265  nn0prpw  32293  filnetlem4  32351  df3nandALT2  32372  bj-ssbn  32616  bj-cleljustab  32822  bj-sbeq  32871  bj-csbsnlem  32873  bj-elsngl  32931  bj-eltag  32940  bj-tagex  32950  bj-projun  32957  bj-disj2r  32988  bj-restuni  33025  bj-eldiag  33062  bj-eldiag2  33063  topdifinffinlem  33166  relowlpssretop  33183  phpreu  33364  poimirlem24  33404  poimirlem26  33406  poimirlem30  33410  areacirclem5  33475  isbnd2  33553  sbcalf  33888  sbcexf  33889  sbccom2  33901  sbccom2f  33902  sbccom2fi  33903  csbcom2fi  33905  prtlem70  33958  prtlem16  33973  ishlat2  34459  polval2N  35011  dicelval3  36288  mapdordlem1a  36742  fz1eqin  37151  7rexfrabdioph  37183  rmydioph  37400  dford4  37415  areaquad  37621  ifpan23  37623  ifpdfnan  37650  ifpdfxor  37651  ifpidg  37655  ifpid1g  37658  ifpim123g  37664  ifp1bi  37666  ifpimimb  37668  ifpororb  37669  ifpbibib  37674  rp-fakenanass  37679  rp-fakeuninass  37681  cllem0  37690  rababg  37698  elmapintrab  37701  elmapintab  37721  undmrnresiss  37729  ss2iundf  37770  dfxor4  37877  rp-imass  37885  dfhe3  37889  dffrege115  38092  frege131  38108  frege133  38110  clsk1indlem4  38162  clsk1indlem1  38163  undisjrab  38325  pm13.196a  38435  eelT11  38752  eelTT1  38755  eelT01  38756  eel0T1  38757  uunTT1  38840  uunTT1p1  38841  uunTT1p2  38842  uunT11  38843  uunT11p1  38844  uunT11p2  38845  uun111  38852  iunssf  39083  ssrabf  39118  rabssf  39122  disjinfi  39196  elicores  39563  fourierdlem42  40129  iundjiun  40440  2reu7  40954  2reu8  40955  dfdfat2  40974  aovov0bi  41039  257prm  41238  fmtno4prmfac  41249  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  uspgrsprf1  41520  opeliun2xp  41876  aacllem  42312
  Copyright terms: Public domain W3C validator