Theorem bitr 173

Description: An inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

Ref	Expression
bitr	⊢ (φ ↔ χ)

Proof of Theorem bitr

Step	Hyp	Ref	Expression
1		bitr.1	. . . 4 ⊢ (φ ↔ ψ)
2	1	biimp 151	. . 3 ⊢ (φ → ψ)
3		bitr.2	. . . 4 ⊢ (ψ ↔ χ)
4	3	biimp 151	. . 3 ⊢ (ψ → χ)
5	2, 4	syl 10	. 2 ⊢ (φ → χ)
6	3	biimpr 152	. . 3 ⊢ (χ → ψ)
7	1	biimpr 152	. . 3 ⊢ (ψ → φ)
8	6, 7	syl 10	. 2 ⊢ (χ → φ)
9	5, 8	impbi 157	1 ⊢ (φ ↔ χ)

Syntax hints:   ↔ wb 146

This theorem is referenced by:  bitr2 174  bitr3 175  bitr4 176  3bitr 177  3bitr2 179  3bitr3 181  3bitr4 183  imbi12i 188  dfor2 229  iman 237  orbi12i 257  or42 265  anor 304  oran 312  impexp 347  pm4.14 352  pm4.78 354  anass 439  anbi12i 481  pm5.53 482  an42 506  pm4.11 520  ibibr 589  orddi 604  anddi 605  bibi12i 608  pm4.71r 634  pm5.18 658  nbbn 659  pm5.17 666  dfbi 668  xor2 671  pm5.55 673  tbt 718  nbn 720  biorfi 734  orbidi 741  biluk 743  ccase 753  ccased 754  prlem2 769  rnlem 771  3orass 776  3anass 777  3ancomb 781  alex 1030  alinexa 1038  exanali 1039  alexn 1040  19.21-2 1053  19.26-2 1064  19.27 1065  19.28 1066  19.36 1074  19.37 1076  19.30 1081  19.44 1085  19.45 1086  alrot4 1093  exrot3 1095  exrot4 1096  albi 1103  2albi 1104  aaan 1115  eeor 1116  sbor 1230  sb19.21 1231  sban 1232  sbbi 1234  sblbis 1235  sbrbis 1236  sbrbif 1237  sbid2 1248  sbco2d 1251  sb8e 1257  19.23vv 1289  19.41vv 1301  19.41vvv 1302  19.42vv 1305  3exdistr 1307  4exdistr 1308  cbvex4v 1317  eeanv 1318  eeeanv 1319  sbcom2 1329  2sb5 1330  2sb6 1331  sb6a 1332  2sb5rf 1333  2sb6rf 1334  sb7f 1336  sbex 1343  sbalv 1344  exsb 1345  2exsb 1346  a12lem2 1370  euf 1377  sb8eu 1383  cbveu 1384  mo 1386  eu2 1389  mo2 1393  mo3 1394  mo4f 1395  eu4 1403  moanim 1420  euan 1421  mopick2 1429  2exeu 1439  2mo 1440  2mos 1441  2eu1 1442  2eu3 1444  2eu4 1445  2eu6 1447  exists1 1450  abid 1458  eqeq12i 1480  eleq12i 1531  abeq2 1560  abeq2i 1562  eq2ab 1565  clabel 1574  sbabel 1576  necon3abii 1588  necon1abii 1608  neanior 1631  ralinexa 1675  rexanali 1676  r3al 1682  r19.26 1742  r19.26-2 1743  r19.43 1757  ralcom 1766  rexcom 1767  ralcom2 1768  reeanv 1770  cbvral2v 1794  cbvral3v 1795  rabeq2i 1801  ceqsex2 1827  vtocl2 1834  vtocl3 1835  vtoclgf 1837  cla4gf 1851  cla43gv 1858  eqvincf 1875  ceqsrex2v 1881  elrab2 1898  euxfr2 1916  euxfr 1917  reu2 1920  rmo4 1923  reu4 1924  reu7 1925  2reuswap 1927  sbralie 1931  sbccomglem 1978  ra5 1990  dfss 2044  ss2ab 2106  dfpss2 2123  psseq12i 2129  pssn2lp 2137  sspsstri 2138  uneqri 2164  ssequn2 2193  unss 2194  ineqri 2199  sseqin2 2219  nssinpss 2230  nsspssun 2231  dfss4 2232  difin 2235  symdif2 2256  inrab2 2262  reuun2 2268  rab0 2283  eq0 2284  0el 2286  0pss 2298  npss0 2299  disj1 2302  disjpss 2309  undif4 2315  difin0ss 2322  inssdif0 2323  r19.3rzv 2338  ralidm 2347  dfpr2 2412  ralpr 2418  rexpr 2419  eusn 2436  eldifsn 2453  difprsn 2456  pw0 2459  pwpw0 2460  eqsn 2465  prsspw 2471  prel12 2475  preqsn 2477  eluniab 2503  elunirab 2504  unipr 2505  uniun 2509  uniin 2510  unissb 2518  elintab 2534  elintrab 2535  ssintab 2540  intun 2552  intpr 2553  iuniin 2563  iuneq2 2568  dfiun2g 2576  dfiin2 2578  iunss 2581  iunid 2593  iun0 2594  0iun 2595  iunxsn 2602  iunun 2603  iunxun 2604  iununi 2606  iunpwss 2608  inex1 2706  pwex 2735  pwssb 2750  exss 2759  dtru 2762  zfpair2 2770  elop 2773  copsexg 2782  opeqsn 2791  opthwiener 2796  opabid 2799  brabg 2807  opabn0 2813  pwunss 2815  pwundif 2817  dfid3 2826  pocl 2835  sotric 2851  so 2855  uniuni 2870  reuxfr2 2893  reuxfr 2894  elpwun 2901  iunpw 2904  dffr2 2909  fr3nr 2916  dfepfr 2922  dfwe2 2925  wefrc 2933  ordtri3or 2969  ordtri2 2972  onintrab2 3004  elsuci 3025  elsucg 3026  sucel 3032  sucid 3041  ordtri2or 3067  ordzsl 3106  onzsl 3107  dflim4 3109  on0eqelt 3114  snsn0non 3115  findsg 3147  tfindsg 3152  elxp 3192  opelxp 3204  brxp 3205  rexxp 3209  ralxpf 3210  opthprc 3211  xpundi 3215  xpundir 3216  xp0r 3229  reluni 3255  relop 3265  opelco 3277  brco 3278  elcnv 3282  elcnv2 3283  eldm2 3297  dmun 3306  dmin 3307  dmi 3315  dmcoss 3347  dmcosseq 3349  rncoeq 3351  resiexg 3380  dfima3 3390  elima2 3393  elima3 3394  imai 3401  imasng 3408  cotr 3420  cnvsym 3421  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  intirr 3427  cnvopab 3431  cnvsn 3435  elxp4 3439  elxp5 3440  imainss 3449  cnvxp 3450  dfrel2 3471  dfrel3 3475  cores 3485  imaco 3487  coi1 3496  coass 3498  relssdr 3499  cnvpo 3508  dffun2 3512  dffun3 3513  dffun4 3514  dffun5 3515  dffun6 3525  dffun8 3527  funopab 3534  funun 3540  funcnv 3543  fun2cnv 3545  fncnv 3547  fun11 3548  fununi 3549  funcnvuni 3550  imadif 3560  funimaexg 3561  isarep1 3563  fnopabg 3601  fnopab2g 3602  fun 3626  fcoi1 3630  fcoi2 3631  fcnvres 3633  fconst 3643  f11 3649  funforn 3663  f1o2 3678  f1ocnv 3686  ffoss 3696  f11o 3697  f1o00 3699  fo00 3700  fv2 3705  elfv 3707  fv3 3718  tz6.12-1 3721  nfvres 3733  fvopab5 3778  dff3 3803  dffo3 3804  dffo5 3806  ffnfvf 3814  fopabfv 3816  fsn2 3821  fconst3 3835  fconst4 3836  funfvima 3837  imaiun 3849  abexssex 3857  f1fv 3859  f1fvf 3860  isoini 3885  tfrlem3 3898  tfrlem7 3902  tfrlem9 3904  dfrdg2 3918  tz7.48lem 3940  tz7.48-2 3942  dfoprab2 3976  dmoprab 3987  rnoprab 3989  resoprab 3994  ffnoprval 3999  fnoprval 4002  foprval 4003  oprabex3 4007  oprabval3 4015  oprabval6g 4017  fooprval 4022  ndmoprdistr 4035  1st2val 4079  2nd2val 4080  2ndconst 4081  curry1 4082  dfopab2 4097  dfoprab3 4098  dfoprab5 4099  foprab2 4103  el1o 4130  oarec 4180  oeordi 4198  oaabs 4236  dfer2 4246  eqerlem 4254  erdisj 4270  elqs 4274  ecid 4284  qsid 4285  brecop 4290  ecopoprsym 4294  th3qlem1 4298  mapval2 4319  elpm 4320  elpm2 4321  mapsn 4329  ixpeq2 4339  domen 4361  en1 4407  2dom 4408  xpsnen 4415  xpcomen 4419  xpassen 4421  pw2en 4426  sbthlem9 4435  sdomdomtr 4449  xpen 4468  mapxpen 4475  xpmapenlem5 4480  ssenen 4484  nneneq 4492  php 4493  0sdom1dom 4504  unfilem1 4524  abfii2 4536  abfii4 4538  iunfi 4543  supmo 4550  zfreg2 4569  inf2 4580  inf3lem2 4586  axinf2 4596  zfinf 4598  trcl 4617  zfregs 4619  setind2 4621  tz9.12lem1 4631  tz9.12lem3 4633  rankel 4652  rankval3 4653  unbndrank 4655  rankun 4663  scottexs 4690  scott0s 4691  cplem1 4692  bnd2 4696  kardex 4697  karden 4698  aceq1 4701  aceq2 4703  aceq3lem 4704  aceq3 4705  aceq4 4706  aceq5lem1 4707  aceq5lem2 4708  aceq5lem3 4709  aceq5lem4 4710  aceq5lem5 4711  aceq6b 4714  ac6n 4729  ac9s 4736  kmlem3 4739  kmlem4 4740  kmlem7 4743  kmlem8 4744  kmlem9 4745  kmlem13 4749  kmlem14 4750  kmlem15 4751  aceqkm 4753  zorn2lem6 4765  brdom7disj 4776  brdom6disj 4777  card1 4805  sucxpdom 4818  iscard 4825  iscard2 4826  alephord2 4848  alephislim 4855  cardaleph 4857  alephval3 4875  cf0 4882  cfeq0 4886  cfsuc 4887  cdaen 4896  cdadom1 4905  elni 4976  ltexpi 5001  ltsopq 5047  genpv 5074  genpn0 5078  genpass 5084  1pr 5089  addcompr 5095  mulcompr 5097  distrlem1pr 5099  distrlem5pr 5103  prlem934b 5110  reclem1pr 5128  reclem2pr 5129  suplem1pr 5133  ltsosr 5175  ltasr 5181  mappsrpr 5190  map2psrpr 5192  suppsr3 5196  opelcn 5220  elreal 5222  axaddopr 5237  axmulopr 5238  axicn 5242  axrnegex 5255  axrrecex 5256  pre-axmulgt0 5262  pre-axsup 5263  subadd2 5345  neg11 5378  1re 5407  ltxrltt 5472  xrlenltt 5473  leloet 5491  xrleloet 5530  xrrebndt 5541  ltadd1 5565  leadd2 5567  addgt0 5572  ltneg 5577  ltnegcon2 5579  msqgt0 5587  msq0 5664  rec11i 5733  divmul24t 5739  halfpos 5852  infm3 6001  infmsup 6015  arch 6018  xrinfmss 6026  supxrre 6030  elnnz 6092  elznn0nn 6095  elznn0 6096  elznn 6097  elnn0nn 6118  elnnnn0 6119  zltp1let 6128  uzwo3 6166  zmin 6167  elq 6195  ralrp 6226  icounlem 6345  snunioolem 6347  raluz2 6375  rexuz2 6377  nnwof 6391  nnwos 6392  sq00 6546  subsq0 6579  nn0le2msqt 6593  nn0opth2 6597  inelr 6665  replimt 6692  abslt 6810  absle 6811  cau4i 6855  cau5 6856  cvg3 6860  bcpasc 6907  dffsum 6936  csbfsum 6965  clm4 7018  climunii 7035  climeu 7037  climshft2 7043  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  mulc1cncf 7214  ef1tllem 7323  eirrlem1 7330  ruclem1 7453  ruclem3 7455  ruclem8 7460  infxpidmlem6 7500  infxpidmlem7 7501  infxpidmlem9 7503  infxpidmlem12 7506  infmap2lem1 7521  infmap2lem2 7522  alephsuc3 7527  istps4 7551  istps5 7552  isbasis2g 7554  tgval2t 7559  tgval3t 7567  tgss3t 7580  basgent 7582  clsval2 7627  elcls 7646  ntreq0 7650  islp2 7688  islpi 7690  cncnplem4 7716  sncld 7726  blrn2 7782  cncfmet 7844  metcn4 7905  fsumcnlem 7923  bcthlem7 7939  bcthlem29 7961  bcthlem32 7964  grpidinvlem3 7984  sspval 8316  isphg 8407  isph 8412  siii 8444  ishl 8522  spwmo 8580  pilem1 8590  sincosq1lem 8620  cosh111lem1 8629  cosh111lem3 8631  efifolem4 8640  effoi 8666  effoiOLD 8667  grothinf 8720  grothprimlem 8721  grothprim 8722  avril1 8723  h2hcau 8788  hvsubadd 8854  normsub0 8923  bcsALT 8967  hhcmpl 8990  hlimunii 9029  chcmh 9034  norm1ex 9043  elch0 9047  pjthlem1 9134  omlsilem 9159  pjoc2 9186  chsscon1 9300  chsscon2 9301  spanun 9382  h1deot 9387  h1det 9388  elspansn 9397  cmcm4 9455  cmbr3 9460  cmbr4 9461  osumlem5 9499  osumcor2 9507  5oalem7 9522  3oalem3 9526  pjss2 9542  mayete3 9590  cnvadj 9733  nmopunt 9854  nmcopexlem1 9866  lncnopbd 9881  nmcfnexlem1 9895  riesz2t 9914  bra11 9954  pjnmop 9986  pjssdif1 10014  pjin2 10031  pjin3 10032  pjclem1 10033  strlem1 10087  cvbr2t 10120  cvnbtwn3t 10125  cvnbtwn4t 10126  mdsl2b 10158  mdsldmd1 10166  elat2 10175  chrelat2 10200  chrelat4 10208  atoml 10217  irred 10229  mdsymlem6 10243  mdsymlem8 10245  sumdmdi 10249  dmdbr5at 10255  cdj3 10273  elghom 10289  ghomgrpilem2 10291  cayleylem2 10317  cayleylem3 10318  19.41vvvv 10335  eeeeanv 10336  r19.3rzvb 10337  ntunte 10340  ficli 10368  bsi 10382  hmeogrp 10425  subsp 10429  ishoma 10559  ismonc 10584  blkssatm 10603

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 147

Copyright terms: Public domain