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

Theorem 3bitr4i 269
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 244 . 2  |-  ( ph  <->  th )
51, 4bitri 241 1  |-  ( ch  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  bibi2d  310  or4  515  pm4.14  562  pm4.71  612  pm5.32ri  620  an31  776  an4  798  orimdi  821  ordi  835  ordir  836  andir  839  dfbi3  864  orbidi  899  3anrot  941  3orrot  942  3ancoma  943  3orcoma  944  3orcomb  946  3ioran  952  3anbi123i  1142  3orbi123i  1143  an6  1263  3or6  1265  nancom  1296  xorcom  1313  xorass  1314  xorneg2  1318  xorbi12i  1320  hadbi  1393  hadcoma  1394  hadcomb  1395  cador  1397  cadan  1398  hadnot  1399  cadnot  1400  cadcoma  1401  cadcomb  1402  cad1  1404  nic-axALT  1445  nfbii  1575  19.26-3an  1602  19.43OLD  1613  cbvexvw  1710  excom  1748  equsalhw  1850  19.32  1885  19.31  1886  19.42  1891  4exdistr  1923  eeeanv  1927  eeeanvOLD  1928  equsal  1954  equsexOLD  1958  cbvex  2020  dfsb3  2089  sbor  2099  sban  2102  sbbi  2104  sb6  2132  pm11.07OLD  2149  sbel2x  2159  sbex  2162  sb8eu  2256  sb8mo  2257  eu1  2259  sbmo  2268  cbvmo  2275  moanim  2294  eqcom  2389  abeq1  2493  cbvab  2505  clelab  2507  nfceqi  2519  sbabel  2549  ralbii2  2677  rexbii2  2678  r2alf  2684  r2exf  2685  r3al  2706  r19.30  2796  r19.32v  2797  r19.41  2803  r19.42v  2805  r19.43  2806  ralcomf  2809  rexcomf  2810  reean  2817  3reeanv  2819  2ralor  2820  rabid2  2828  rabbi  2829  reubiia  2836  rmobiia  2841  reu5  2864  rmo5  2867  cbvralf  2869  cbvrexf  2870  cbvreu  2873  cbvrmo  2874  vjust  2900  ceqsex3v  2937  ceqsex4v  2938  ceqsex8v  2940  eueq  3049  reu2  3065  reu6  3066  reu3  3067  rmo4  3070  2reu5  3085  cbvsbc  3132  sbccomlem  3174  rmo3  3191  csbabg  3253  cbvralcsf  3254  cbvrexcsf  3255  cbvreucsf  3256  eqss  3306  uniiunlem  3374  sspsstri  3392  ssequn1  3460  unss  3464  rexun  3470  ralunb  3471  elin3  3475  incom  3476  inass  3494  ssin  3506  nssinpss  3516  dfun2  3519  difin  3521  indi  3530  indifdir  3540  symdif2  3550  rabn0  3590  disj3  3615  ssdif0  3629  inssdif0  3638  ssundif  3654  dfif2  3684  snprc  3814  reusn  3820  difsnpss  3884  prss  3895  tpss  3907  pwpr  3953  eluni2  3961  elunirab  3970  uniun  3976  unissb  3987  elintrab  4004  ssintrab  4015  intun  4024  intpr  4025  iuncom  4041  iuncom4  4042  iunab  4078  ssiinf  4081  iunn0  4092  iinab  4093  iunin2  4096  iinun2  4098  iundif2  4099  iunun  4112  iunxun  4113  iunxiun  4114  sspwuni  4117  iinpw  4120  cbvdisj  4133  disjor  4137  brun  4199  brin  4200  brdif  4201  dftr2  4245  intexrab  4300  inuni  4303  ssext  4359  pweqb  4361  otth2  4380  opelopabsbOLD  4404  eqopab2b  4425  pwin  4428  pwun  4432  dflim2  4578  unisuc  4598  reusv5OLD  4673  reusv7OLD  4675  sucexb  4729  sucelon  4737  dflim4  4768  xpiundi  4872  xpiundir  4873  poinxp  4881  soinxp  4882  frinxp  4883  seinxp  4884  weinxp  4885  inopab  4945  difopab  4946  raliunxp  4954  rexiunxp  4955  rexxpf  4960  iunxpf  4961  cnvco  4996  dmiun  5018  dmuni  5019  dm0rn0  5026  brres  5092  dmres  5107  cnvsym  5188  asymref  5190  codir  5194  qfto  5195  cnvopab  5214  cnvdif  5218  rniun  5222  dminss  5226  imainss  5227  dmsnn0  5275  cnvcnvsn  5287  resco  5314  imaco  5315  rnco  5316  coiun  5319  coass  5328  ressn  5348  cnviin  5349  cnvpo  5350  cnvso  5351  xpco  5354  funcnv  5451  funcnv3  5452  fncnv  5455  fun11  5456  imadif  5468  fnres  5501  dfmpt3  5507  fnopabg  5508  fint  5562  fin  5563  fores  5602  dff1o3  5620  fun11iun  5635  f11o  5648  f1ompt  5830  fsn  5845  opabex3d  5928  opabex3  5929  imaiun  5931  isocnv2  5990  isocnv3  5991  isores2  5992  isomin  5996  eqoprab2b  6071  difxp  6319  dfopab2  6340  dfoprab3s  6341  fmpt2x  6356  fparlem1  6385  fparlem2  6386  fsplit  6390  tpostpos  6435  dfsmo2  6545  brwitnlem  6687  oarec  6741  qsid  6906  uniinqs  6920  mapval2  6979  map0e  6987  mapsncnv  6996  elixp2  7002  ixpin  7023  brsdom  7066  brdom2  7073  xpassen  7138  brsdom2  7167  unfilem1  7307  fiint  7319  dfsup2  7382  supmo  7390  rankc1  7729  cp  7748  isinfcard  7906  aceq1  7931  aceq2  7933  dfac5lem3  7939  dfac10b  7952  dfac12a  7961  dffin7-2  8211  dfacfin7  8212  fin1a2lem6  8218  iunfo  8347  konigthlem  8376  axgroth6  8636  axgroth3  8639  sstskm  8650  ltexprlem1  8846  gt0srpr  8886  ltpsrpr  8917  map2psrpr  8918  ltresr  8948  fimaxre3  9889  sup3  9897  supmul1  9905  elnn0z  10226  elznn0nn  10227  zmin  10502  xrnemnf  10650  xrnepnf  10651  elioomnf  10931  elxrge0  10940  elfzuzb  10985  elfz2nn0  11014  fzass4  11022  elfzo2  11073  elfzo3  11085  lbfzo0  11100  fzind2  11125  nn0opthlem1  11488  rexfiuz  12078  fsumcom2  12485  sinltx  12717  divalglem4  12843  divalglem10  12849  isprm2lem  13013  4sqlem12  13251  imasleval  13693  xpsfrnel  13715  xpscf  13718  isssc  13947  isffth2  14040  ispos2  14332  ismhm  14667  nsgacs  14903  isgim  14976  oppgcntz  15087  efgrelexlemb  15309  pgpfac1  15565  pgpfac  15569  opprsubg  15668  opprunit  15693  isirred2  15733  opprirred  15734  drngprop  15773  opprdrng  15786  islss  15938  islbs  16075  isdomn2  16286  unocv  16830  iunocv  16831  istps2OLD  16909  isbasis2g  16936  tgval2  16944  ntreq0  17064  isclo2  17075  cmpcov2  17375  is1stc2  17426  1stcelcls  17445  llyi  17458  txuni2  17518  xkobval  17539  hausdiag  17598  isfbas2  17788  elfg  17824  fbasrn  17837  fmfnfmlem3  17909  isfcls  17962  alexsubALTlem2  18000  istmd  18025  istgp  18028  istrg  18114  istdrg  18116  istdrg2  18128  isms2  18370  metuel2  18485  restmetu  18489  isngp  18514  isngp2  18515  isngp3  18516  elii1  18831  iscph  19004  isbn  19160  pmltpc  19214  ovolfcl  19230  finiunmbl  19305  iundisj  19309  dyaddisj  19355  vitalilem1  19367  ellimc3  19633  ig1pval3  19964  plyun0  19983  plydivex  20081  aannenlem2  20113  ellogrn  20324  atandm  20583  atandm3  20585  atans2  20638  issubgo  21739  h2hlm  22331  issh  22558  chcon2i  22814  chcon1i  22815  chcon3i  22816  chnlei  22835  cmcm2i  22943  cmcm3i  22944  3oalem3  23014  pjdifnormii  23033  pjneli  23073  dfadj2  23236  cnvadj  23243  hhcno  23255  hhcnf  23256  eleigvec  23308  eleigvec2  23309  pjimai  23527  isst  23564  ishst  23565  cvnbtwn4  23640  chrelat4i  23724  rabid2f  23811  rmo3f  23826  rmo4fOLD  23827  cbvdisjf  23859  disjorf  23865  iundisjf  23872  disjexc  23876  mptfnf  23915  xrdifh  23979  iundisjfi  23990  eldifpr  24188  cntnevol  24376  ballotlemodife  24534  erdszelem1  24656  cvmliftlem15  24764  snmlval  24797  untuni  24937  dfso3  24956  prodmo  25041  dftr6  25131  coep  25132  coepr  25133  dffr5  25134  dfso2  25135  dfpo2  25136  cnvco1  25141  cnvco2  25142  eldm3  25143  dfdm5  25156  dfrn5  25157  wfrlem8  25287  wfrlem11  25290  tfrALTlem  25300  frrlem5c  25311  elno3  25333  nofulllem5  25384  elsymdif  25391  symdifass  25395  brsset  25453  idsset  25454  dfon3  25456  dfbigcup2  25463  dffix2  25469  dfom5b  25476  dffun10  25477  elfuns  25478  dfiota3  25486  fnimage  25492  brdomain  25496  brrange  25497  brimg  25500  brapply  25501  funpartlem  25505  brrestrict  25512  tfrqfree  25514  altopelaltxp  25535  colinearalg  25563  axeuclid  25616  df3nandALT1  25860  imnand2  25863  supaddc  25947  itg2addnclem2  25958  trer  26010  filnetlem4  26101  inixp  26121  prdstotbnd  26194  heibor1lem  26209  isrngohom  26272  isidl  26315  isfldidl2  26370  isdmn3  26375  moxfr  26424  fphpd  26568  f1omvdco3  27061  issdrg2  27175  pm10.541  27231  compab  27312  conss34  27313  r19.32  27613  rmoanim  27625  bnj257  28409  bnj268  28411  bnj290  28412  bnj312  28414  bnj89  28424  bnj538  28446  bnj887  28472  bnj976  28486  bnj1019  28488  bnj1146  28500  bnj1385  28542  bnj110  28567  bnj121  28579  bnj130  28583  bnj153  28589  bnj543  28602  bnj580  28622  bnj607  28625  bnj849  28634  bnj882  28635  bnj916  28642  bnj985  28662  bnj1033  28676  bnj1083  28685  bnj1090  28686  bnj1128  28697  bnj1174  28710  bnj1228  28718  equsexNEW7  28828  cbvexwAUX7  28856  sborNEW7  28902  sbanNEW7  28905  sbbiNEW7  28906  sb8ewAUX7  28927  sb6NEW7  28930  sbel2xNEW7  28947  sbexNEW7  28950  dfsb3NEW7  28972  eeeanvOLD7  29020  cbvexOLD7  29042  sb8eOLD7  29073  pmapglbx  29883  lhpexle3  30126  cdleme25cv  30472  dicelval3  31295  diclspsn  31309  lcfls1c  31651
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 178
  Copyright terms: Public domain W3C validator