Theorem bitri 171

Description: An inference from transitive law for logical equivalence.

Hypotheses

Ref	Expression
bitri.1	⊢ (φ ↔ ψ)
bitri.2	⊢ (ψ ↔ χ)

Assertion

Ref	Expression
bitri	⊢ (φ ↔ χ)

Proof of Theorem bitri

Step	Hyp	Ref	Expression
1		bitri.1	. . . 4 ⊢ (φ ↔ ψ)
2	1	biimpi 149	. . 3 ⊢ (φ → ψ)
3		bitri.2	. . . 4 ⊢ (ψ ↔ χ)
4	3	biimpi 149	. . 3 ⊢ (ψ → χ)
5	2, 4	syl 10	. 2 ⊢ (φ → χ)
6	3	biimpri 150	. . 3 ⊢ (χ → ψ)
7	1	biimpri 150	. . 3 ⊢ (ψ → φ)
8	6, 7	syl 10	. 2 ⊢ (χ → φ)
9	5, 8	impbii 155	1 ⊢ (φ ↔ χ)

Syntax hints:   ↔ wb 144

This theorem is referenced by:  bitr2i 172  bitr3i 173  bitr4i 174  3bitri 175  3bitr2i 177  3bitr3i 179  3bitr4i 181  imbi12i 186  dfor2 227  iman 235  orbi12i 255  or42 263  anor 302  oran 310  impexp 345  pm4.14 350  pm4.78 352  anass 441  anbi12i 485  pm5.53 486  an42 510  notbi 525  ibibr 594  orddi 609  anddi 610  bibi12i 613  pm4.71r 639  pm5.18 663  nbbn 664  pm5.17 671  dfbi3 673  xor2 676  xordi 678  pm5.55 679  tbt 725  nbn 727  biorfi 741  orbidi 748  biluk 750  ccase 760  ccased 761  prlem2 776  rnlem 778  3orass 784  3anass 785  3ancomb 789  nic-justbi 964  nic-mpALT 968  nic-axALT 970  alex 1070  alinexa 1078  exanali 1079  alexn 1080  19.21-2 1093  19.26-2 1104  19.27 1105  19.28 1106  19.36 1114  19.37 1116  19.30 1121  19.44 1125  19.45 1126  alrot4 1133  exrot3 1135  exrot4 1136  albi 1143  2albi 1144  aaan 1155  eeor 1156  sbor 1272  sb19.21 1273  sban 1274  sbbi 1276  sblbis 1277  sbrbis 1278  sbrbif 1279  sbid2 1291  sbco2d 1294  sb8e 1300  19.23vv 1332  19.41vv 1344  19.41vvv 1345  19.42vv 1348  3exdistr 1350  4exdistr 1351  cbvex4v 1360  eeanv 1361  eeeanv 1362  sbcom2 1373  2sb5 1374  2sb6 1375  sb6a 1376  2sb5rf 1377  2sb6rf 1378  sb7f 1380  sbex 1387  sbalv 1388  exsb 1389  2exsb 1390  a12lem2 1416  euf 1423  sb8eu 1429  cbveu 1430  mo 1432  eu2 1435  mo2 1439  mo3 1440  mo4f 1441  eu4 1449  moanim 1466  euan 1467  mopick2 1476  2exeu 1486  2mo 1487  2mos 1488  2eu1 1489  2eu3 1491  2eu4 1492  2eu6 1494  exists1 1498  abid 1507  eqeq12i 1531  eleq12i 1582  abeq2 1611  abeq2i 1613  eq2ab 1616  clabel 1625  sbabel 1627  necon3abii 1639  necon1abii 1660  neanior 1685  ralinexa 1729  rexanali 1730  r3al 1736  r19.26 1796  r19.26-2 1797  r19.43 1811  ralcom 1820  rexcom 1821  ralcom2 1822  reeanv 1824  cbvral2v 1849  cbvral3v 1850  rabeq2i 1856  ceqsex2 1882  vtocl2 1889  vtocl3 1890  vtoclgf 1892  cla4gf 1906  cla43gv 1913  eqvincf 1930  ceqsrex2v 1936  elrab2 1953  euxfr2 1972  euxfr 1973  reu2 1976  rmo4 1979  reu4 1980  reu7 1981  2reuswap 1983  sbralie 1986  sbccomglem 2038  ra5 2050  dfss 2106  ss2ab 2168  dfpss2 2185  psseq12i 2191  pssn2lp 2199  sspsstri 2200  uneqri 2226  ssequn2 2255  unss 2256  ineqri 2261  sseqin2 2281  nssinpss 2292  nsspssun 2293  dfss4 2294  difin 2297  symdif2 2318  inrab2 2324  reuun2 2330  rab0 2346  eq0 2347  0el 2349  0pss 2361  npss0 2362  disj1 2365  disjpss 2372  undif4 2378  difin0ss 2385  inssdif0 2386  r19.3rzv 2402  ralidm 2411  pwss 2466  dfpr2 2480  ralpr 2486  rexpr 2487  ralsng 2489  eusn 2507  eldifsn 2526  difprsn 2529  pw0 2532  pwpw0 2533  eqsn 2539  prsspw 2545  prel12 2549  preqsn 2551  pwsnALT 2566  eluniab 2579  elunirab 2580  unipr 2581  uniun 2586  uniin 2587  unissb 2595  elintab 2611  elintrab 2612  ssintab 2617  intun 2629  intpr 2630  iuniin 2641  iuneq2 2646  dfiun2g 2654  dfiin2 2656  iunss 2659  iun0 2672  0iun 2673  iunxsn 2682  iunun 2683  iunxun 2684  iununi 2686  pwssb 2688  iunpwss 2691  inex1 2790  axpweq 2817  pwex 2823  exss 2847  dtruALT 2848  zfpair2 2856  elop 2859  copsexg 2868  opcom 2877  opeqsn 2879  opthwiener 2884  opabid 2887  brabg 2895  opelopabf 2899  opabn0 2902  pwunss 2904  pwundif 2906  dfid3 2914  pocl 2922  posn 2928  sotric 2939  so 2943  dffr2 2949  dfepfr 2960  wefrc 2970  ordtri3or 3007  ordtri2 3010  elsuci 3039  elsucg 3040  sucel 3046  sucid 3051  ordtri2or 3067  on0eqel 3087  snsn0non 3088  uniuni 3104  reuxfr2 3126  reuxfr 3127  elpwun 3134  iunpw 3137  fr3nr 3138  dfwe2 3140  onintrab2 3159  ordzsl 3199  onzsl 3200  dflim4 3202  tfindsg 3213  findsg 3245  elxp 3283  opelxp 3297  brxp 3298  rexxp 3302  ralxpf 3303  rexxpf 3304  iunxpf 3305  opthprc 3306  xpundi 3310  xpundir 3311  elvvv 3314  xp0r 3325  eqrelrel 3341  reliun 3354  reluni 3356  relop 3365  opelco 3378  brco 3379  elcnv 3384  elcnv2 3385  eldm2 3399  dmun 3408  dmin 3409  dmi 3415  dmcoss 3450  dmcosseq 3452  rncoeq 3454  resiexg 3486  dfima3 3498  elima2 3501  elima3 3502  imai 3509  imasng 3516  cotr 3528  cnvsym 3529  asymref 3531  asymref2 3532  intirr 3533  cnvopab 3537  imainss 3548  cnvxp 3549  dfrel2 3569  dmsnn0 3573  rnsnn0 3574  cnvsn 3580  elxp4 3585  elxp5 3586  dfrel3 3587  dfco2 3598  coundi 3600  coundir 3601  cores 3602  imaco 3604  coiun 3608  coi1 3614  coass 3616  relssdmrn 3617  relrelss 3618  cnvpo 3627  dffun2 3631  dffun3 3632  dffun4 3633  dffun5 3634  dffun7 3644  dffun9 3646  funopab 3653  funun 3659  funcnv 3662  fun2cnv 3664  fncnv 3666  fun11 3667  fununi 3668  funcnvuni 3669  imadif 3679  funimaexg 3681  isarep1 3683  fnopabg 3722  fnopab2g 3723  fun 3748  fcoi1 3752  fcoi2 3753  fcnvres 3755  fconst 3765  dff12 3771  funforn 3786  dff1o2 3801  f1ocnv 3809  resdif 3816  ffoss 3822  f11o 3823  f1o00 3825  fo00 3826  fv2 3831  elfv 3833  fv3 3844  tz6.12-1 3847  nfvres 3859  fvopab5 3904  fvopab6 3905  dff4 3932  dffo3 3933  dffo5 3935  ffnfvf 3943  fopabfv 3945  fsn2 3950  fconst3 3964  fconst4 3965  funfvima 3966  imaiun 3978  abexssex 3986  dff13 3988  dff13f 3989  isoini 4014  dfoprab2 4050  dmoprab 4062  rnoprab 4064  resoprab 4069  ffnoprv 4074  fnoprv 4077  foprv 4078  oprabex3 4082  oprabval3 4090  oprabval6g 4093  fooprv 4098  ndmoprdistr 4110  dfopab2 4173  dfoprab3 4174  dfoprab5sf 4178  foprab2 4181  curry1 4193  curry2 4196  fsplit 4204  tfrlem3 4214  tfrlem7 4218  tfrlem9 4220  dfrdg2 4234  tz7.48lem 4256  tz7.48-2 4258  el1o 4282  oarec 4332  oeordi 4350  oaabs 4392  dfer2 4402  eqerlem 4410  erdisj 4426  uniqs 4436  0nelqs 4439  ecid 4441  qsid 4442  brecop 4447  ecopoprsym 4451  th3qlem1 4455  mapval2 4476  elpm 4477  elpm2 4478  mapsn 4486  ixpeq2 4496  domen 4520  isfi 4523  en1 4567  2dom 4568  xpsnen 4576  xpcomen 4580  xpassen 4582  pw2en 4587  ac6sfilem3 4590  sbthlem9 4600  sdomdomtr 4614  pwuninel 4631  2pwuninel 4632  xpen 4635  mapxpen 4642  xpmapenlem5 4647  ssenen 4651  nneneq 4659  php 4660  0sdom1dom 4671  unfilem1 4694  abfii2 4705  abfii4 4707  iunfi 4712  supmo 4719  zfreg2 4740  inf2 4753  inf3lem2 4759  axinf2 4769  zfinf2 4771  trcl 4791  zfregs 4793  setind2 4795  tz9.12lem1 4805  tz9.12lem3 4807  rankel 4826  rankval3 4827  unbndrank 4829  rankun 4837  scottexs 4864  scott0s 4865  cplem1 4866  bnd2 4870  kardex 4871  karden 4872  aceq1 4875  aceq2 4877  aceq3lem 4878  aceq3 4879  aceq4 4880  aceq5lem1 4881  aceq5lem2 4882  aceq5lem3 4883  aceq5lem4 4884  aceq5lem5 4885  aceq6b 4888  ac6n 4903  ac9s 4910  kmlem3 4913  kmlem4 4914  kmlem7 4917  kmlem8 4918  kmlem9 4919  kmlem13 4923  kmlem14 4924  kmlem15 4925  aceqkm 4927  zorn2lem6 4939  brdom7disj 4950  brdom6disj 4951  card1 4981  sucxpdom 4996  iscard 5003  iscard2 5004  alephord2 5026  alephislim 5033  cardaleph 5035  alephval3 5053  cf0 5060  cfeq0 5064  cfsuc 5065  cdaen 5075  cdadom1 5085  elni 5158  ltexpi 5183  ltsopq 5229  genpv 5256  genpn0 5260  genpass 5266  1pr 5271  addcompr 5277  mulcompr 5279  distrlem1pr 5281  distrlem5pr 5285  prlem934b 5292  reclem1pr 5310  reclem2pr 5311  suplem1pr 5315  ltsosr 5357  ltasr 5363  mappsrpr 5372  map2psrpr 5374  suppsr3 5378  opelcn 5402  elreal 5404  axaddopr 5419  axmulopr 5420  axicn 5424  axrnegex 5437  axrrecex 5438  pre-axmulgt0 5444  pre-axsup 5445  subadd2i 5527  neg11i 5560  1re 5589  ltxrlt 5654  xrlenlt 5655  leloe 5672  xrleloe 5711  xrrebnd 5722  ltadd1i 5745  leadd2i 5747  addgt0i 5752  ltnegi 5757  ltnegcon2i 5759  msqgt0i 5767  msq0i 5847  rec11ii 5916  halfposi 6049  ralrp 6205  infm3 6222  infmsup 6236  arch 6239  xrinfmss 6247  supxrre 6251  elnnz 6313  elznn0nn 6316  elznn0 6317  elznn 6318  elnn0nn 6339  elnnnn0 6340  zltp1le 6349  uzwo3 6390  zmin 6391  elq 6396  icounlem 6539  snunioolem 6541  raluz2 6570  rexuz2 6572  nnwof 6586  nnwos 6587  subsq0i 6845  nn0le2msqi 6864  nn0opth2i 6868  inelr 6936  replim 6962  abslti 7078  abslei 7079  cau4ii 7121  cau5i 7122  cvg3i 7126  bcpasci 7172  dffsum 7201  csbfsum 7230  clm4i 7283  climunii 7301  climeu 7303  climshft2i 7309  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  mulc1cncf 7484  ef1tllem 7586  eirrlem1 7594  ruclem1 7722  ruclem3 7724  ruclem8 7729  infxpidmlem6 7769  infxpidmlem7 7770  infxpidmlem9 7772  infxpidmlem12 7775  infmap2lem1 7791  infmap2lem2 7792  alephsuc3 7797  istps4 7821  istps5 7822  isbasis2g 7824  tgval2 7829  tgval3 7837  tgss3 7850  basgen 7852  clsval2 7895  elcls 7914  ntreq0 7918  islp2 7957  islpi 7959  cncnplem4 7987  sncld 7997  blrn2 8052  cncfmet 8116  metcn4 8182  fsumcnlem 8200  bcthlem7 8216  bcthlem29 8238  bcthlem32 8241  grpidinvlem3 8263  sspval 8636  isphg 8732  isph 8737  siii 8769  ishl 8851  spwmo 8918  spwpr2 8920  pilem1 8938  sincosq1lem 8970  cosh111lem1 8986  cosh111lem3 8988  efifolem4 8997  effoi 9017  grothinf 9053  grothpw 9054  axgroth5 9055  grothprimlem 9056  grothprim 9057  avril1 9058  h2hcau 9124  axhcompl 9143  hvsubaddi 9208  normsub0i 9278  bcsiALT 9322  hhcmpl 9345  hlimuniii 9384  chcmhi 9389  norm1exi 9398  elch0 9402  hhsssh2 9416  pjthlem1 9495  omlsilem 9520  pjoc2i 9547  chsscon1i 9661  chsscon2i 9662  spanuni 9743  h1deoi 9748  h1dei 9749  elspansni 9757  cmcm4i 9814  cmbr3i 9819  cmbr4i 9820  osumlem5 9860  osumcor2i 9868  5oalem7 9883  3oalem3 9887  pjss2i 9903  mayete3i 9951  mayete3OLDi 9952  cnvadj 10096  nmopun 10218  nmcopexlem1 10230  lncnopbd 10245  nmcfnexlem1 10259  riesz2 10278  nmopcoadj0i 10315  bra11 10321  pjnmopi 10355  pjssdif1i 10383  pjin2i 10402  pjin3i 10403  pjclem1 10404  strlem1 10458  cvbr2 10491  cvnbtwn3 10496  cvnbtwn4 10497  mdsl2bi 10531  mdsldmd1i 10539  elat2 10548  chrelat2i 10573  chrelat4i 10581  atomli 10591  irredi 10603  mdsymlem6 10617  mdsymlem8 10619  sumdmdii 10624  dmdbr5ati 10631  cdj3i 10650  xfree2 10654  elghom 10669  ghomgrpilem2 10671  cayleylem2 10695  cayleylem3 10696  anddi2 10718  19.41vvvv 10719  eeeeanv 10720  r19.3rzvb 10721  ntunte 10728  ficli 10756  cnvref 10769  ref3w 10772  twpar2 10773  restidsing 10805  bsi 10995  hmeogrp 11044  subsp 11056  rcfpfillem2 11090  limfillem1 11101  altretoplem2 11143  altretop 11144  ishoma 11242  ismonc 11269  isepic 11279  issubcat 11299  3anor 11389  ecase13d 11391  dfiin2g 11400  cnvresima 11407  dmsdtriord 11408  trer 11409  finminlem 11418  elfiun 11421  fictblem 11422  fictb 11423  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  infenomsub 11450  opncldf1 11454  opncldf3 11456  clsun 11465  subntr 11482  cnsubsp 11483  compsub 11488  cptclsscpt 11489  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  is1stc3 11530  is2ndc2 11534  isfne2 11542  topfneec 11562  fnessref 11564  locfincomp 11575  comppfsc 11578  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  ist0-2 11600  isfbas2 11622  fbssint 11626  fbasfip 11627  fbunfip 11631  elfg 11633  extbas1 11641  filrn 11643  neifg 11644  isufil2 11650  ufprim 11654  filssufillem 11655  fixufil 11661  ufinffr 11663  filcon 11665  hausfillim 11685  cnpfillim 11686  elfilmap 11690  rnelfmlem 11698  flimfcn 11715  isfclus 11718  fcluscf 11724  flimfnfcls 11727  fcluscn 11731  fclsfcn 11744  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  gapmlem 11783  sbmo 11787  unpreima 11794  respreima 11795  opabex3 11806  oprabopabf 11807  eqfnfv3 11819  inixp 11820  fimax 11837  indexf 11847  fzm1 11867  elnnr 11874  sdc 11877  fsum00 11883  fsumltisumi 11886  lmclim2 11915  piececn 11955  txbas 11973  uptx 11978  sstotbnd 11992  isbnd3 11997  heiborlem1 12011  heiborlem16 12026  heiborlem20 12030  heiborlem37 12047  bfp 12065  rrndstprj 12073  rrntotbndlem1 12076  rrntotbnd 12078  phtpycolem5 12097  phtpyco 12098  blkssatm 12193  subdefbi1 12221

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain