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

Theorem 3bitr4i 270
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 245 . 2  |-  ( ph  <->  th )
51, 4bitri 242 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  bibi2d  311  or4  516  pm4.14  563  pm4.71  613  pm5.32ri  621  an31  777  an4  799  orimdi  822  ordi  836  ordir  837  andir  840  dfbi3  865  orbidi  900  3anrot  942  3orrot  943  3ancoma  944  3orcoma  945  3orcomb  947  3ioran  953  3anbi123i  1143  3orbi123i  1144  an6  1264  3or6  1266  nancom  1300  xorcom  1317  xorass  1318  xorneg2  1322  xorbi12i  1324  hadbi  1397  hadcoma  1398  hadcomb  1399  cador  1401  cadan  1402  hadnot  1403  cadnot  1404  cadcoma  1405  cadcomb  1406  cad1  1408  nic-axALT  1449  nfbii  1579  19.26-3an  1606  19.43OLD  1617  cbvexvw  1718  excom  1757  equsalhw  1861  19.32  1897  19.31  1898  19.42  1903  4exdistr  1935  eeeanv  1939  eeeanvOLD  1940  cbvex  1984  equsal  2000  equsexOLD  2004  dfsb3  2110  sbor  2139  sban  2140  sbbi  2142  sb6  2176  pm11.07OLD  2193  sbel2x  2203  sbex  2206  sb8eu  2300  sb8mo  2301  eu1  2303  sbmo  2312  cbvmo  2319  moanim  2338  eqcom  2439  abeq1  2543  cbvab  2555  clelab  2557  nfceqi  2569  sbabel  2599  ralbii2  2734  rexbii2  2735  r2alf  2741  r2exf  2742  r3al  2764  r19.30  2854  r19.32v  2855  r19.41  2861  r19.42v  2863  r19.43  2864  ralcomf  2867  rexcomf  2868  reean  2875  3reeanv  2877  2ralor  2878  rabid2  2886  rabbi  2887  reubiia  2894  rmobiia  2899  reu5  2922  rmo5  2925  cbvralf  2927  cbvrexf  2928  cbvreu  2931  cbvrmo  2932  vjust  2958  ceqsex3v  2995  ceqsex4v  2996  ceqsex8v  2998  eueq  3107  reu2  3123  reu6  3124  reu3  3125  rmo4  3128  2reu5  3143  cbvsbc  3190  sbccomlem  3232  rmo3  3249  csbabg  3311  cbvralcsf  3312  cbvrexcsf  3313  cbvreucsf  3314  eqss  3364  uniiunlem  3432  sspsstri  3450  ssequn1  3518  unss  3522  rexun  3528  ralunb  3529  elin3  3533  incom  3534  inass  3552  ssin  3564  nssinpss  3574  dfun2  3577  difin  3579  indi  3588  indifdir  3598  symdif2  3608  rabn0  3648  disj3  3673  ssdif0  3687  inssdif0  3696  ssundif  3712  dfif2  3742  snprc  3872  reusn  3878  difsnpss  3942  prss  3953  tpss  3965  pwpr  4012  eluni2  4020  elunirab  4029  uniun  4035  unissb  4046  elintrab  4063  ssintrab  4074  intun  4083  intpr  4084  iuncom  4100  iuncom4  4101  iunab  4138  ssiinf  4141  iunn0  4152  iinab  4153  iunin2  4156  iinun2  4158  iundif2  4159  iunun  4172  iunxun  4173  iunxiun  4174  sspwuni  4177  iinpw  4180  cbvdisj  4193  disjor  4197  brun  4259  brin  4260  brdif  4261  dftr2  4305  intexrab  4360  inuni  4363  ssext  4419  pweqb  4421  otth2  4440  opelopabsbOLD  4464  eqopab2b  4485  pwin  4488  pwun  4492  dflim2  4638  unisuc  4658  reusv5OLD  4734  reusv7OLD  4736  sucexb  4790  sucelon  4798  dflim4  4829  xpiundi  4933  xpiundir  4934  poinxp  4942  soinxp  4943  frinxp  4944  seinxp  4945  weinxp  4946  inopab  5006  difopab  5007  raliunxp  5015  rexiunxp  5016  rexxpf  5021  iunxpf  5022  cnvco  5057  dmiun  5079  dmuni  5080  dm0rn0  5087  brres  5153  dmres  5168  cnvsym  5249  asymref  5251  codir  5255  qfto  5256  cnvopab  5275  cnvdif  5279  rniun  5283  dminss  5287  imainss  5288  dmsnn0  5336  cnvcnvsn  5348  resco  5375  imaco  5376  rnco  5377  coiun  5380  coass  5389  ressn  5409  cnviin  5410  cnvpo  5411  cnvso  5412  xpco  5415  funcnv  5512  funcnv3  5513  fncnv  5516  fun11  5517  imadif  5529  fnres  5562  dfmpt3  5568  fnopabg  5569  fint  5623  fin  5624  fores  5663  dff1o3  5681  fun11iun  5696  f11o  5709  f1ompt  5892  fsn  5907  opabex3d  5990  opabex3  5991  imaiun  5993  isocnv2  6052  isocnv3  6053  isores2  6054  isomin  6058  eqoprab2b  6133  difxp  6381  dfopab2  6402  dfoprab3s  6403  fmpt2x  6418  fparlem1  6447  fparlem2  6448  fsplit  6452  tpostpos  6500  dfsmo2  6610  brwitnlem  6752  oarec  6806  qsid  6971  uniinqs  6985  mapval2  7044  map0e  7052  mapsncnv  7061  elixp2  7067  ixpin  7088  brsdom  7131  brdom2  7138  xpassen  7203  brsdom2  7232  unfilem1  7372  fiint  7384  dfsup2  7448  supmo  7458  rankc1  7797  cp  7816  isinfcard  7974  aceq1  7999  aceq2  8001  dfac5lem3  8007  dfac10b  8020  dfac12a  8029  dffin7-2  8279  dfacfin7  8280  fin1a2lem6  8286  iunfo  8415  konigthlem  8444  axgroth6  8704  axgroth3  8707  sstskm  8718  ltexprlem1  8914  gt0srpr  8954  ltpsrpr  8985  map2psrpr  8986  ltresr  9016  fimaxre3  9958  sup3  9966  supmul1  9974  elnn0z  10295  elznn0nn  10296  zmin  10571  xrnemnf  10719  xrnepnf  10720  elioomnf  11000  elxrge0  11009  elfzuzb  11054  elfz2nn0  11083  fzass4  11091  elfzo2  11144  elfzo3  11156  lbfzo0  11171  fzind2  11199  nn0opthlem1  11562  rexfiuz  12152  fsumcom2  12559  sinltx  12791  divalglem4  12917  divalglem10  12923  isprm2lem  13087  4sqlem12  13325  imasleval  13767  xpsfrnel  13789  xpscf  13792  isssc  14021  isffth2  14114  ispos2  14406  ismhm  14741  nsgacs  14977  isgim  15050  oppgcntz  15161  efgrelexlemb  15383  pgpfac1  15639  pgpfac  15643  opprsubg  15742  opprunit  15767  isirred2  15807  opprirred  15808  drngprop  15847  opprdrng  15860  islss  16012  islbs  16149  isdomn2  16360  unocv  16908  iunocv  16909  istps2OLD  16987  isbasis2g  17014  tgval2  17022  ntreq0  17142  isclo2  17153  cmpcov2  17454  is1stc2  17506  1stcelcls  17525  llyi  17538  txuni2  17598  xkobval  17619  hausdiag  17678  isfbas2  17868  elfg  17904  fbasrn  17917  fmfnfmlem3  17989  isfcls  18042  alexsubALTlem2  18080  istmd  18105  istgp  18108  istrg  18194  istdrg  18196  istdrg2  18208  isms2  18481  metuel2  18610  restmetu  18618  isngp  18644  isngp2  18645  isngp3  18646  elii1  18961  iscph  19134  isbn  19292  pmltpc  19348  ovolfcl  19364  finiunmbl  19439  iundisj  19443  dyaddisj  19489  vitalilem1  19501  ellimc3  19767  ig1pval3  20098  plyun0  20117  plydivex  20215  aannenlem2  20247  ellogrn  20458  atandm  20717  atandm3  20719  atans2  20772  issubgo  21892  h2hlm  22484  issh  22711  chcon2i  22967  chcon1i  22968  chcon3i  22969  chnlei  22988  cmcm2i  23096  cmcm3i  23097  3oalem3  23167  pjdifnormii  23186  pjneli  23226  dfadj2  23389  cnvadj  23396  hhcno  23408  hhcnf  23409  eleigvec  23461  eleigvec2  23462  pjimai  23680  isst  23717  ishst  23718  cvnbtwn4  23793  chrelat4i  23877  rabid2f  23968  rmo3f  23983  rmo4fOLD  23984  cbvdisjf  24016  disjorf  24022  iundisjf  24030  disjexc  24034  mptfnf  24074  xrdifh  24144  iundisjfi  24153  xrnarchi  24255  eldifpr  24393  cntnevol  24583  ballotlemodife  24756  erdszelem1  24878  cvmliftlem15  24986  snmlval  25019  untuni  25159  dfso3  25178  prodmo  25263  fprodcom2  25309  dftr6  25374  coep  25375  coepr  25376  dffr5  25377  dfso2  25378  dfpo2  25379  cnvco1  25384  cnvco2  25385  eldm3  25386  socnv  25389  dfdm5  25401  dfrn5  25402  wfrlem8  25546  wfrlem11  25549  frrlem5c  25589  elno3  25611  nofulllem5  25662  elsymdif  25669  symdifass  25673  brsset  25735  idsset  25736  dfon3  25738  dfbigcup2  25745  dfom5b  25758  dffun10  25760  dfiota3  25769  fnimage  25775  brdomain  25779  brrange  25780  brimg  25783  brapply  25784  brcup  25785  brcap  25786  funpartlem  25788  brrestrict  25795  tfrqfree  25797  brub  25800  altopelaltxp  25822  colinearalg  25850  axeuclid  25903  df3nandALT1  26147  imnand2  26150  supaddc  26238  ismblfin  26248  mbfposadd  26255  itg2addnclem2  26258  ftc1anc  26289  trer  26320  filnetlem4  26411  inixp  26431  prdstotbnd  26504  heibor1lem  26519  isrngohom  26582  isidl  26625  isfldidl2  26680  isdmn3  26685  moxfr  26734  fphpd  26878  f1omvdco3  27370  issdrg2  27484  pm10.541  27540  compab  27621  conss34  27622  r19.32  27922  rmoanim  27934  usgra2pth0  28313  usgreg2spot  28457  bnj257  29072  bnj268  29074  bnj290  29075  bnj312  29077  bnj89  29087  bnj538  29109  bnj887  29135  bnj976  29149  bnj1019  29151  bnj1146  29163  bnj1385  29205  bnj110  29230  bnj121  29242  bnj130  29246  bnj153  29252  bnj543  29265  bnj580  29285  bnj607  29288  bnj849  29297  bnj882  29298  bnj916  29305  bnj985  29325  bnj1033  29339  bnj1083  29348  bnj1090  29349  bnj1128  29360  bnj1174  29373  bnj1228  29381  equsexNEW7  29491  cbvexwAUX7  29521  sborNEW7  29567  sbanNEW7  29570  sbbiNEW7  29571  sb8ewAUX7  29595  sb6NEW7  29598  sbel2xNEW7  29615  sbexNEW7  29618  dfsb3NEW7  29640  eeeanvOLD7  29705  cbvexOLD7  29727  sb8eOLD7  29758  pmapglbx  30567  lhpexle3  30810  cdleme25cv  31156  dicelval3  31979  diclspsn  31993  lcfls1c  32335
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 179
  Copyright terms: Public domain W3C validator