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  1713  excom  1752  equsalhw  1856  19.32  1892  19.31  1893  19.42  1898  4exdistr  1930  eeeanv  1934  eeeanvOLD  1935  equsal  1966  equsexOLD  1970  cbvex  2060  dfsb3  2113  sbor  2123  sban  2126  sbbi  2128  sb6  2156  pm11.07OLD  2173  sbel2x  2183  sbex  2186  sb8eu  2280  sb8mo  2281  eu1  2283  sbmo  2292  cbvmo  2299  moanim  2318  eqcom  2414  abeq1  2518  cbvab  2530  clelab  2532  nfceqi  2544  sbabel  2574  ralbii2  2702  rexbii2  2703  r2alf  2709  r2exf  2710  r3al  2731  r19.30  2821  r19.32v  2822  r19.41  2828  r19.42v  2830  r19.43  2831  ralcomf  2834  rexcomf  2835  reean  2842  3reeanv  2844  2ralor  2845  rabid2  2853  rabbi  2854  reubiia  2861  rmobiia  2866  reu5  2889  rmo5  2892  cbvralf  2894  cbvrexf  2895  cbvreu  2898  cbvrmo  2899  vjust  2925  ceqsex3v  2962  ceqsex4v  2963  ceqsex8v  2965  eueq  3074  reu2  3090  reu6  3091  reu3  3092  rmo4  3095  2reu5  3110  cbvsbc  3157  sbccomlem  3199  rmo3  3216  csbabg  3278  cbvralcsf  3279  cbvrexcsf  3280  cbvreucsf  3281  eqss  3331  uniiunlem  3399  sspsstri  3417  ssequn1  3485  unss  3489  rexun  3495  ralunb  3496  elin3  3500  incom  3501  inass  3519  ssin  3531  nssinpss  3541  dfun2  3544  difin  3546  indi  3555  indifdir  3565  symdif2  3575  rabn0  3615  disj3  3640  ssdif0  3654  inssdif0  3663  ssundif  3679  dfif2  3709  snprc  3839  reusn  3845  difsnpss  3909  prss  3920  tpss  3932  pwpr  3979  eluni2  3987  elunirab  3996  uniun  4002  unissb  4013  elintrab  4030  ssintrab  4041  intun  4050  intpr  4051  iuncom  4067  iuncom4  4068  iunab  4105  ssiinf  4108  iunn0  4119  iinab  4120  iunin2  4123  iinun2  4125  iundif2  4126  iunun  4139  iunxun  4140  iunxiun  4141  sspwuni  4144  iinpw  4147  cbvdisj  4160  disjor  4164  brun  4226  brin  4227  brdif  4228  dftr2  4272  intexrab  4327  inuni  4330  ssext  4386  pweqb  4388  otth2  4407  opelopabsbOLD  4431  eqopab2b  4452  pwin  4455  pwun  4459  dflim2  4605  unisuc  4625  reusv5OLD  4700  reusv7OLD  4702  sucexb  4756  sucelon  4764  dflim4  4795  xpiundi  4899  xpiundir  4900  poinxp  4908  soinxp  4909  frinxp  4910  seinxp  4911  weinxp  4912  inopab  4972  difopab  4973  raliunxp  4981  rexiunxp  4982  rexxpf  4987  iunxpf  4988  cnvco  5023  dmiun  5045  dmuni  5046  dm0rn0  5053  brres  5119  dmres  5134  cnvsym  5215  asymref  5217  codir  5221  qfto  5222  cnvopab  5241  cnvdif  5245  rniun  5249  dminss  5253  imainss  5254  dmsnn0  5302  cnvcnvsn  5314  resco  5341  imaco  5342  rnco  5343  coiun  5346  coass  5355  ressn  5375  cnviin  5376  cnvpo  5377  cnvso  5378  xpco  5381  funcnv  5478  funcnv3  5479  fncnv  5482  fun11  5483  imadif  5495  fnres  5528  dfmpt3  5534  fnopabg  5535  fint  5589  fin  5590  fores  5629  dff1o3  5647  fun11iun  5662  f11o  5675  f1ompt  5858  fsn  5873  opabex3d  5956  opabex3  5957  imaiun  5959  isocnv2  6018  isocnv3  6019  isores2  6020  isomin  6024  eqoprab2b  6099  difxp  6347  dfopab2  6368  dfoprab3s  6369  fmpt2x  6384  fparlem1  6413  fparlem2  6414  fsplit  6418  tpostpos  6466  dfsmo2  6576  brwitnlem  6718  oarec  6772  qsid  6937  uniinqs  6951  mapval2  7010  map0e  7018  mapsncnv  7027  elixp2  7033  ixpin  7054  brsdom  7097  brdom2  7104  xpassen  7169  brsdom2  7198  unfilem1  7338  fiint  7350  dfsup2  7413  supmo  7421  rankc1  7760  cp  7779  isinfcard  7937  aceq1  7962  aceq2  7964  dfac5lem3  7970  dfac10b  7983  dfac12a  7992  dffin7-2  8242  dfacfin7  8243  fin1a2lem6  8249  iunfo  8378  konigthlem  8407  axgroth6  8667  axgroth3  8670  sstskm  8681  ltexprlem1  8877  gt0srpr  8917  ltpsrpr  8948  map2psrpr  8949  ltresr  8979  fimaxre3  9921  sup3  9929  supmul1  9937  elnn0z  10258  elznn0nn  10259  zmin  10534  xrnemnf  10682  xrnepnf  10683  elioomnf  10963  elxrge0  10972  elfzuzb  11017  elfz2nn0  11046  fzass4  11054  elfzo2  11106  elfzo3  11118  lbfzo0  11133  fzind2  11161  nn0opthlem1  11524  rexfiuz  12114  fsumcom2  12521  sinltx  12753  divalglem4  12879  divalglem10  12885  isprm2lem  13049  4sqlem12  13287  imasleval  13729  xpsfrnel  13751  xpscf  13754  isssc  13983  isffth2  14076  ispos2  14368  ismhm  14703  nsgacs  14939  isgim  15012  oppgcntz  15123  efgrelexlemb  15345  pgpfac1  15601  pgpfac  15605  opprsubg  15704  opprunit  15729  isirred2  15769  opprirred  15770  drngprop  15809  opprdrng  15822  islss  15974  islbs  16111  isdomn2  16322  unocv  16870  iunocv  16871  istps2OLD  16949  isbasis2g  16976  tgval2  16984  ntreq0  17104  isclo2  17115  cmpcov2  17415  is1stc2  17466  1stcelcls  17485  llyi  17498  txuni2  17558  xkobval  17579  hausdiag  17638  isfbas2  17828  elfg  17864  fbasrn  17877  fmfnfmlem3  17949  isfcls  18002  alexsubALTlem2  18040  istmd  18065  istgp  18068  istrg  18154  istdrg  18156  istdrg2  18168  isms2  18441  metuel2  18570  restmetu  18578  isngp  18604  isngp2  18605  isngp3  18606  elii1  18921  iscph  19094  isbn  19252  pmltpc  19308  ovolfcl  19324  finiunmbl  19399  iundisj  19403  dyaddisj  19449  vitalilem1  19461  ellimc3  19727  ig1pval3  20058  plyun0  20077  plydivex  20175  aannenlem2  20207  ellogrn  20418  atandm  20677  atandm3  20679  atans2  20732  issubgo  21852  h2hlm  22444  issh  22671  chcon2i  22927  chcon1i  22928  chcon3i  22929  chnlei  22948  cmcm2i  23056  cmcm3i  23057  3oalem3  23127  pjdifnormii  23146  pjneli  23186  dfadj2  23349  cnvadj  23356  hhcno  23368  hhcnf  23369  eleigvec  23421  eleigvec2  23422  pjimai  23640  isst  23677  ishst  23678  cvnbtwn4  23753  chrelat4i  23837  rabid2f  23928  rmo3f  23943  rmo4fOLD  23944  cbvdisjf  23976  disjorf  23982  iundisjf  23990  disjexc  23994  mptfnf  24034  xrdifh  24104  iundisjfi  24113  xrnarchi  24215  eldifpr  24353  cntnevol  24543  ballotlemodife  24716  erdszelem1  24838  cvmliftlem15  24946  snmlval  24979  untuni  25119  dfso3  25138  prodmo  25223  fprodcom2  25269  dftr6  25329  coep  25330  coepr  25331  dffr5  25332  dfso2  25333  dfpo2  25334  cnvco1  25339  cnvco2  25340  eldm3  25341  dfdm5  25354  dfrn5  25355  wfrlem8  25485  wfrlem11  25488  tfrALTlem  25498  frrlem5c  25509  elno3  25531  nofulllem5  25582  elsymdif  25589  symdifass  25593  brsset  25651  idsset  25652  dfon3  25654  dfbigcup2  25661  dffix2  25667  dfom5b  25674  dffun10  25675  elfuns  25676  dfiota3  25684  fnimage  25690  brdomain  25694  brrange  25695  brimg  25698  brapply  25699  funpartlem  25703  brrestrict  25710  tfrqfree  25712  altopelaltxp  25733  colinearalg  25761  axeuclid  25814  df3nandALT1  26058  imnand2  26061  supaddc  26145  ismblfin  26154  mbfposadd  26161  itg2addnclem2  26164  trer  26217  filnetlem4  26308  inixp  26328  prdstotbnd  26401  heibor1lem  26416  isrngohom  26479  isidl  26522  isfldidl2  26577  isdmn3  26582  moxfr  26631  fphpd  26775  f1omvdco3  27268  issdrg2  27382  pm10.541  27438  compab  27519  conss34  27520  r19.32  27820  rmoanim  27832  usgra2pth0  28050  usgreg2spot  28178  bnj257  28789  bnj268  28791  bnj290  28792  bnj312  28794  bnj89  28804  bnj538  28826  bnj887  28852  bnj976  28866  bnj1019  28868  bnj1146  28880  bnj1385  28922  bnj110  28947  bnj121  28959  bnj130  28963  bnj153  28969  bnj543  28982  bnj580  29002  bnj607  29005  bnj849  29014  bnj882  29015  bnj916  29022  bnj985  29042  bnj1033  29056  bnj1083  29065  bnj1090  29066  bnj1128  29077  bnj1174  29090  bnj1228  29098  equsexNEW7  29208  cbvexwAUX7  29236  sborNEW7  29282  sbanNEW7  29285  sbbiNEW7  29286  sb8ewAUX7  29307  sb6NEW7  29310  sbel2xNEW7  29327  sbexNEW7  29330  dfsb3NEW7  29352  eeeanvOLD7  29400  cbvexOLD7  29422  sb8eOLD7  29453  pmapglbx  30263  lhpexle3  30506  cdleme25cv  30852  dicelval3  31675  diclspsn  31689  lcfls1c  32031
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