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

Theorem 3bitr4i 268
Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
3bitr4i.1  |-  ( ph  <->  ps )
3bitr4i.2  |-  ( ch  <->  ph )
3bitr4i.3  |-  ( th  <->  ps )
Assertion
Ref Expression
3bitr4i  |-  ( ch  <->  th )

Proof of Theorem 3bitr4i
StepHypRef Expression
1 3bitr4i.2 . 2  |-  ( ch  <->  ph )
2 3bitr4i.1 . . 3  |-  ( ph  <->  ps )
3 3bitr4i.3 . . 3  |-  ( th  <->  ps )
42, 3bitr4i 243 . 2  |-  ( ph  <->  th )
51, 4bitri 240 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  bibi2d  309  or4  514  pm4.14  561  pm4.71  611  pm5.32ri  619  an31  775  an4  797  orimdi  820  ordi  834  ordir  835  andir  838  dfbi3  863  orbidi  898  3anrot  939  3orrot  940  3ancoma  941  3orcoma  942  3orcomb  944  3ioran  950  3anbi123i  1140  3orbi123i  1141  an6  1261  3or6  1263  nancom  1290  xorcom  1298  xorass  1299  xorneg2  1303  xorbi12i  1305  hadbi  1377  hadcoma  1378  hadcomb  1379  cador  1381  cadan  1382  hadnot  1383  cadnot  1384  cadcoma  1385  cadcomb  1386  cad1  1388  nic-axALT  1429  nfbii  1556  19.26-3an  1582  19.43OLD  1593  cbvexvw  1677  19.32  1811  19.31  1812  19.42  1816  eeeanv  1855  equsex  1902  cbvex  1925  dfsb3  1996  sbor  2006  sban  2009  sbbi  2011  sb8e  2033  sb6  2038  pm11.07  2054  sbel2x  2064  sbex  2067  sb8eu  2161  sb8mo  2162  eu1  2164  sbmo  2173  cbvmo  2180  moanim  2199  eqcom  2285  abeq1  2389  cbvab  2401  clelab  2403  nfceqi  2415  sbabel  2445  ralbii2  2571  rexbii2  2572  r2alf  2578  r2exf  2579  r3al  2600  r19.30  2685  r19.32v  2686  r19.41  2692  r19.42v  2694  r19.43  2695  ralcomf  2698  rexcomf  2699  reean  2706  3reeanv  2708  2ralor  2709  rabid2  2717  rabbi  2718  reubiia  2725  rmobiia  2730  reu5  2753  rmo5  2756  cbvralf  2758  cbvrexf  2759  cbvreu  2762  cbvrmo  2763  vjust  2789  ceqsex3v  2826  ceqsex4v  2827  ceqsex8v  2829  eueq  2937  reu2  2953  reu6  2954  reu3  2955  rmo4  2958  2reu5  2973  cbvsbc  3019  sbccomlem  3061  rmo3  3078  csbabg  3142  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  eqss  3194  uniiunlem  3260  sspsstri  3278  ssequn1  3345  unss  3349  rexun  3355  ralunb  3356  elin3  3360  incom  3361  inass  3379  ssin  3391  nssinpss  3401  dfun2  3404  difin  3406  indi  3415  indifdir  3425  symdif2  3434  rabn0  3474  disj3  3499  ssdif0  3513  inssdif0  3521  ssundif  3537  dfif2  3567  snprc  3695  reusn  3700  difsnpss  3758  prss  3769  tpss  3779  pwpr  3823  eluni2  3831  elunirab  3840  uniun  3846  unissb  3857  elintrab  3874  ssintrab  3885  intun  3894  intpr  3895  iuncom  3911  iuncom4  3912  iunab  3948  ssiinf  3951  iunn0  3962  iinab  3963  iunin2  3966  iinun2  3968  iundif2  3969  iunun  3982  iunxun  3983  iunxiun  3984  sspwuni  3987  iinpw  3990  cbvdisj  4003  disjor  4007  brun  4069  brin  4070  brdif  4071  dftr2  4115  intexrab  4170  inuni  4173  ssext  4228  pweqb  4230  otth2  4249  opelopabsbOLD  4273  eqopab2b  4294  pwin  4297  pwun  4302  dflim2  4448  unisuc  4468  reusv2lem4  4538  reusv5OLD  4544  reusv7OLD  4546  sucexb  4600  sucelon  4608  dflim4  4639  xpiundi  4743  xpiundir  4744  poinxp  4753  soinxp  4754  frinxp  4755  seinxp  4756  weinxp  4757  inopab  4816  difopab  4817  raliunxp  4825  rexiunxp  4826  rexxpf  4831  iunxpf  4832  cnvco  4865  dmiun  4887  dmuni  4888  dm0rn0  4895  brres  4961  dmres  4976  cnvsym  5057  asymref  5059  codir  5063  qfto  5064  cnvopab  5083  cnvdif  5087  rniun  5091  dminss  5095  imainss  5096  dmsnn0  5138  cnvcnvsn  5150  resco  5177  imaco  5178  rnco  5179  coiun  5182  coass  5191  ressn  5211  cnviin  5212  cnvpo  5213  cnvso  5214  funcnv  5310  funcnv3  5311  fncnv  5314  fun11  5315  imadif  5327  fnres  5360  dfmpt3  5366  fnopabg  5367  fint  5420  fin  5421  fores  5460  dff1o3  5478  fun11iun  5493  f11o  5506  f1ompt  5682  fsn  5696  opabex3  5769  imaiun  5771  isocnv2  5828  isocnv3  5829  isores2  5830  isomin  5834  eqoprab2b  5906  difxp  6153  dfopab2  6174  dfoprab3s  6175  fmpt2x  6190  fparlem1  6218  fparlem2  6219  fsplit  6223  tpostpos  6254  dfsmo2  6364  brwitnlem  6506  oarec  6560  qsid  6725  mapval2  6797  map0e  6805  mapsncnv  6814  elixp2  6820  ixpin  6841  brsdom  6884  brdom2  6891  xpassen  6956  brsdom2  6985  unfilem1  7121  fiint  7133  dfsup2  7195  supmo  7203  rankc1  7542  cp  7561  isinfcard  7719  aceq1  7744  aceq2  7746  dfac5lem3  7752  dfac10b  7765  dfac12a  7774  dffin7-2  8024  dfacfin7  8025  fin1a2lem6  8031  iunfo  8161  konigthlem  8190  axgroth6  8450  axgroth3  8453  sstskm  8464  ltexprlem1  8660  gt0srpr  8700  ltpsrpr  8731  map2psrpr  8732  ltresr  8762  fimaxre3  9703  sup3  9711  supmul1  9719  elnn0z  10036  elznn0nn  10037  zmin  10312  xrnemnf  10460  xrnepnf  10461  elioomnf  10738  elxrge0  10747  elfzuzb  10792  elfz2nn0  10821  fzass4  10829  elfzo2  10878  elfzo3  10890  lbfzo0  10903  fzind2  10923  nn0opthlem1  11283  rexfiuz  11831  fsumcom2  12237  sinltx  12469  divalglem4  12595  divalglem10  12601  isprm2lem  12765  4sqlem12  13003  imasleval  13443  xpsfrnel  13465  xpscf  13468  isffth2  13790  ispos2  14082  ismhm  14417  nsgacs  14653  isgim  14726  oppgcntz  14837  efgrelexlemb  15059  pgpfac1  15315  pgpfac  15319  opprsubg  15418  opprunit  15443  isirred2  15483  opprirred  15484  drngprop  15523  opprdrng  15536  islss  15692  islbs  15829  isdomn2  16040  unocv  16580  iunocv  16581  istps2OLD  16659  isbasis2g  16686  tgval2  16694  ntreq0  16814  isclo2  16825  cmpcov2  17117  is1stc2  17168  1stcelcls  17187  llyi  17200  txuni2  17260  xkobval  17281  hausdiag  17339  isfbas2  17530  elfg  17566  fbasrn  17579  fmfnfmlem3  17651  isfcls  17704  alexsubALTlem2  17742  istmd  17757  istgp  17760  istrg  17846  istdrg  17848  istdrg2  17860  isms2  17996  isngp  18118  isngp2  18119  isngp3  18120  elii1  18433  iscph  18606  isbn  18760  pmltpc  18810  ovolfcl  18826  finiunmbl  18901  iundisj  18905  dyaddisj  18951  vitalilem1  18963  ellimc3  19229  ig1pval3  19560  plyun0  19579  plydivex  19677  aannenlem2  19709  ellogrn  19917  atandm  20172  atandm3  20174  atans2  20227  issubgo  20970  h2hlm  21560  issh  21787  chcon2i  22043  chcon1i  22044  chcon3i  22045  chnlei  22064  cmcm2i  22172  cmcm3i  22173  3oalem3  22243  pjdifnormii  22262  pjneli  22302  dfadj2  22465  cnvadj  22472  hhcno  22484  hhcnf  22485  eleigvec  22537  eleigvec2  22538  pjimai  22756  isst  22793  ishst  22794  cvnbtwn4  22869  chrelat4i  22953  ballotlemodife  23056  rabid2f  23135  cntnevol  23175  rmo3f  23178  rmo4fOLD  23179  mptfnf  23226  xrdifh  23273  cbvdisjf  23350  disjorf  23356  iundisjfi  23363  iundisjf  23365  eldifpr  23394  erdszelem1  23722  cvmliftlem15  23829  snmlval  23914  untuni  24055  dfso3  24074  dftr6  24107  coep  24108  coepr  24109  dffr5  24110  dfso2  24111  dfpo2  24112  cnvco1  24117  cnvco2  24118  eldm3  24119  dfdm5  24132  dfrn5  24133  wfrlem8  24263  wfrlem11  24266  tfrALTlem  24276  frrlem5c  24287  elno3  24309  nofulllem5  24360  elsymdif  24367  symdifass  24371  brsset  24429  idsset  24430  dfon3  24432  dfbigcup2  24439  dffix2  24445  dfom5b  24452  dffun10  24453  elfuns  24454  dfiota3  24462  fnimage  24468  brdomain  24472  brrange  24473  brimg  24476  brapply  24477  brrestrict  24487  tfrqfree  24489  altopelaltxp  24510  colinearalg  24538  axeuclid  24591  df3nandALT1  24835  imnand2  24838  fates  24955  evevifev  25014  uninqs  25039  elo  25041  restidsing  25076  dff1o6f  25092  cmpdom  25143  trooo  25394  isidlNEW  25446  cinvlem3  25830  cnvresimaOLD  26226  trer  26227  filnetlem4  26330  inixp  26399  prdstotbnd  26518  heibor1lem  26533  isrngohom  26596  isidl  26639  isfldidl2  26694  isdmn3  26699  moxfr  26752  fphpd  26899  f1omvdco3  27392  issdrg2  27506  pm10.541  27562  compab  27644  conss34  27645  r19.32  27945  rmoanim  27957  bnj257  28732  bnj268  28734  bnj290  28735  bnj312  28737  bnj89  28747  bnj538  28769  bnj887  28795  bnj976  28809  bnj1019  28811  bnj1146  28823  bnj1385  28865  bnj110  28890  bnj121  28902  bnj130  28906  bnj153  28912  bnj543  28925  bnj580  28945  bnj607  28948  bnj849  28957  bnj882  28958  bnj916  28965  bnj985  28985  bnj1033  28999  bnj1083  29008  bnj1090  29009  bnj1128  29020  bnj1174  29033  bnj1228  29041  equsexv-x12  29113  pmapglbx  29958  lhpexle3  30201  cdleme25cv  30547  dicelval3  31370  diclspsn  31384  lcfls1c  31726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator