Theorem bitr 173

Description: An inference from transitive law for logical equivalence.

Hypotheses

Ref	Expression
bitr.1	|- (ph <-> ps)
bitr.2	|- (ps <-> ch)

Assertion

Ref	Expression
bitr	|- (ph <-> ch)

Proof of Theorem bitr

Step	Hyp	Ref	Expression
1		bitr.1	. . . 4 |- (ph <-> ps)
2	1	biimp 151	. . 3 |- (ph -> ps)
3		bitr.2	. . . 4 |- (ps <-> ch)
4	3	biimp 151	. . 3 |- (ps -> ch)
5	2, 4	syl 10	. 2 |- (ph -> ch)
6	3	biimpr 152	. . 3 |- (ch -> ps)
7	1	biimpr 152	. . 3 |- (ps -> ph)
8	6, 7	syl 10	. 2 |- (ch -> ph)
9	5, 8	impbi 157	1 |- (ph <-> ch)

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 657  nbbn 658  pm5.17 665  dfbi 667  xor2 670  pm5.55 672  tbt 717  nbn 719  biorfi 733  orbidi 740  biluk 742  ccase 752  ccased 753  prlem2 768  rnlem 770  3orass 775  3anass 776  3ancomb 780  alex 1010  alinexa 1018  exanali 1019  alexn 1020  19.21-2 1033  19.26-2 1044  19.27 1045  19.28 1046  19.36 1054  19.37 1056  19.30 1061  19.44 1065  19.45 1066  alrot4 1073  exrot3 1075  exrot4 1076  albi 1083  2albi 1084  aaan 1095  eeor 1096  sbor 1219  sb19.21 1220  sban 1221  sbbi 1223  sblbis 1224  sbrbis 1225  sbrbif 1226  sbid2 1237  sbco2d 1240  sb8e 1246  19.23vv 1276  19.41vv 1288  19.41vvv 1289  19.42vv 1292  3exdistr 1294  4exdistr 1295  cbvex4v 1304  eeanv 1305  eeeanv 1306  sbcom2 1316  2sb5 1317  2sb6 1318  sb6a 1319  2sb5rf 1320  2sb6rf 1321  sb7f 1323  sbex 1330  sbalv 1331  exsb 1332  2exsb 1333  a12lem2 1354  euf 1361  sb8eu 1367  cbveu 1368  mo 1370  eu2 1373  mo2 1377  mo3 1378  mo4f 1379  eu4 1387  moanim 1404  euan 1405  mopick2 1413  2exeu 1423  2mo 1424  2mos 1425  2eu1 1426  2eu3 1428  2eu4 1429  2eu6 1431  exists1 1434  abid 1442  eqeq12i 1464  eleq12i 1515  abeq2 1544  abeq2i 1546  eq2ab 1549  clabel 1558  sbabel 1560  necon3abii 1572  necon1abii 1592  neanior 1615  ralinexa 1659  rexanali 1660  r3al 1666  r19.26 1726  r19.26-2 1727  r19.43 1741  ralcom 1750  rexcom 1751  ralcom2 1752  reeanv 1754  cbvral2v 1778  cbvral3v 1779  rabeq2i 1785  ceqsex2 1811  vtocl2 1818  vtocl3 1819  vtoclgf 1821  cla4gf 1835  eqvincf 1856  ceqsrex2v 1862  elrab2 1879  euxfr2 1897  euxfr 1898  reu2 1901  rmo4 1904  reu4 1905  reu7 1906  2reuswap 1908  sbralie 1912  sbccomglem 1959  ra5 1971  dfss 2025  ss2ab 2087  dfpss2 2104  psseq12i 2110  pssn2lp 2118  sspsstri 2119  uneqri 2145  ssequn2 2174  unss 2175  ineqri 2180  sseqin2 2200  nssinpss 2211  nsspssun 2212  dfss4 2213  difin 2216  symdif2 2237  inrab2 2243  reuun2 2249  rab0 2264  eq0 2265  0el 2267  0pss 2279  npss0 2280  disj1 2283  disjpss 2290  undif4 2296  difin0ss 2303  inssdif0 2304  r19.3rzv 2319  ralidm 2328  dfpr2 2393  ralpr 2399  rexpr 2400  eusn 2416  eldifsn 2432  difprsn 2435  pw0 2438  pwpw0 2439  eqsn 2444  prsspw 2450  prel12 2454  eluniab 2481  elunirab 2482  unipr 2483  uniun 2487  uniin 2488  unissb 2496  elintab 2512  elintrab 2513  ssintab 2518  intun 2530  intpr 2531  iuniin 2541  iuneq2 2546  dfiun2g 2554  dfiin2 2556  iunss 2559  iunid 2571  iun0 2572  0iun 2573  iunxsn 2580  iunun 2581  iunxun 2582  iununi 2584  iunpwss 2586  inex1 2684  pwex 2713  pwssb 2728  exss 2737  dtru 2740  zfpair2 2748  elop 2751  copsexg 2759  opthwiener 2770  opabid 2772  brabg 2780  opabn0 2786  pwunss 2788  pwundif 2790  dfid3 2799  pocl 2808  sotric 2824  so 2828  uniuni 2843  reuxfr2 2866  reuxfr 2867  elpwun 2874  iunpw 2877  dffr2 2882  fr3nr 2889  dfepfr 2895  dfwe2 2898  wefrc 2906  ordtri3or 2942  ordtri2 2945  onintrab2 2977  elsuci 2998  elsucg 2999  sucel 3005  sucid 3014  ordtri2or 3040  ordzsl 3079  onzsl 3080  dflim4 3082  on0eqelt 3087  snsn0non 3088  findsg 3120  tfindsg 3125  elxp 3165  opelxp 3176  brxp 3177  rexxp 3181  ralxpf 3182  opthprc 3183  xpundi 3187  xpundir 3188  xp0r 3201  reluni 3227  opelco 3245  brco 3246  elcnv 3250  elcnv2 3251  eldm2 3265  dmun 3274  dmin 3275  dmi 3283  dmcoss 3314  dmcosseq 3316  rncoeq 3318  resiexg 3347  dfima3 3357  elima2 3360  elima3 3361  imai 3368  imasng 3375  cotr 3387  cnvsym 3388  intirr 3390  cnvopab 3394  cnvsn 3398  elxp4 3402  elxp5 3403  imainss 3412  cnvxp 3413  dfrel2 3431  cores 3441  imaco 3443  coi1 3452  coass 3454  relssdr 3455  cnvpo 3463  dffun2 3467  dffun3 3468  dffun4 3469  dffun5 3470  dffun6 3480  dffun8 3482  funopab 3488  funun 3494  funcnv 3497  fun2cnv 3499  fncnv 3501  fun11 3502  fununi 3503  funcnvuni 3504  imadif 3514  funimaexg 3515  isarep1 3517  fnopabg 3555  fnopab2g 3556  fun 3580  fcoi1 3584  fcoi2 3585  fcnvres 3587  fconst 3597  f11 3603  funforn 3617  f1o2 3632  f1ocnv 3640  ffoss 3650  f11o 3651  f1o00 3653  fo00 3654  fv2 3659  elfv 3661  fv3 3672  tz6.12-1 3675  nfvres 3687  fvopab5 3732  dff3 3757  dffo3 3758  dffo5 3760  ffnfvf 3768  fopabfv 3770  fsn2 3775  fconst3 3789  fconst4 3790  funfvima 3791  imaiun 3803  abexssex 3811  f1fv 3813  f1fvf 3814  isoini 3839  tfrlem3 3852  tfrlem7 3856  tfrlem9 3858  dfrdg2 3872  tz7.48lem 3894  tz7.48-2 3896  dfoprab2 3930  dmoprab 3941  rnoprab 3943  resoprab 3948  ffnoprval 3953  fnoprval 3956  foprval 3957  oprabex3 3961  oprabval3 3969  oprabval6g 3971  fooprval 3976  ndmoprdistr 3989  1st2val 4033  2nd2val 4034  2ndconst 4035  curry1 4036  dfopab2 4051  dfoprab3 4052  dfoprab5 4053  foprab2 4057  el1o 4084  oarec 4134  oeordi 4152  oaabs 4190  er2 4200  eqerlem 4208  erdisj 4224  elqs 4228  ecid 4238  qsid 4239  brecop 4244  ecopoprsym 4248  th3qlem1 4252  mapval2 4273  elpm 4274  elpm2 4275  mapsn 4283  ixpeq2 4293  domen 4315  en1 4361  2dom 4362  xpsnen 4369  xpcomen 4373  xpassen 4375  pw2en 4380  sbthlem9 4389  sdomdomtr 4403  xpen 4420  mapxpen 4427  xpmapenlem5 4432  ssenen 4436  nneneq 4444  php 4445  0sdom1dom 4456  unfilem1 4476  abfii2 4488  abfii4 4490  iunfi 4495  supmo 4502  zfreg2 4521  inf2 4532  inf3lem2 4538  axinf2 4548  zfinf 4550  trcl 4569  zfregs 4571  setind2 4573  tz9.12lem1 4583  tz9.12lem3 4585  rankel 4604  rankval3 4605  unbndrank 4607  rankun 4615  scottexs 4642  scott0s 4643  cplem1 4644  bnd2 4648  kardex 4649  karden 4650  aceq1 4653  aceq2 4655  aceq3lem 4656  aceq3 4657  aceq4 4658  aceq5lem1 4659  aceq5lem2 4660  aceq5lem3 4661  aceq5lem4 4662  aceq5lem5 4663  aceq6b 4666  ac6n 4681  ac9s 4688  kmlem3 4691  kmlem4 4692  kmlem7 4695  kmlem8 4696  kmlem9 4697  kmlem13 4701  kmlem14 4702  kmlem15 4703  aceqkm 4705  zorn2lem6 4717  brdom7disj 4728  brdom6disj 4729  sucxpdom 4769  iscard 4776  iscard2 4777  alephord2 4799  alephislim 4806  cardaleph 4808  alephval3 4826  cf0 4833  cfeq0 4837  cfsuc 4838  cdaen 4847  cdadom1 4856  elni 4927  ltexpi 4952  ltsopq 4998  genpv 5025  genpn0 5029  genpass 5035  1pr 5040  addcompr 5046  mulcompr 5048  distrlem1pr 5050  distrlem5pr 5054  prlem934b 5061  reclem1pr 5079  reclem2pr 5080  suplem1pr 5084  ltsosr 5126  ltasr 5132  mappsrpr 5141  map2psrpr 5143  suppsr3 5147  opelcn 5171  elreal 5173  axaddopr 5188  axmulopr 5189  axicn 5193  axrnegex 5206  axrrecex 5207  pre-axmulgt0 5213  pre-axsup 5214  subadd2 5296  neg11 5329  1re 5358  ltxrltt 5423  xrlenltt 5424  leloet 5442  xrleloet 5481  xrrebndt 5492  ltadd1 5516  leadd2 5518  addgt0 5523  ltneg 5528  ltnegcon2 5530  msqgt0 5538  msq0 5615  rec11i 5684  divmul24t 5690  halfpos 5803  infm3 5952  infmsup 5966  arch 5969  xrinfmss 5977  supxrre 5981  elnnz 6043  elznn0nn 6046  elznn0 6047  elznn 6048  elnn0nn 6069  elnnnn0 6070  zltp1let 6079  uzwo3 6117  zmin 6118  elq 6146  ralrp 6177  icounlem 6296  snunioolem 6298  raluz2 6326  rexuz2 6328  nnwof 6342  nnwos 6343  sq00 6497  subsq0 6530  nn0le2msqt 6544  nn0opth2 6548  inelr 6616  replimt 6643  abslt 6761  absle 6762  cau4i 6806  cau5 6807  cvg3 6811  bcpasc 6858  dffsum 6887  csbfsum 6916  clm4 6969  climunii 6986  climeu 6988  climshft2 6994  cvgcmp3cetlem1 7075  cvgcmp3cetlem2 7076  mulc1cncf 7165  ef1tllem 7274  eirrlem1 7281  ruclem1 7404  ruclem3 7406  ruclem8 7411  infxpidmlem6 7451  infxpidmlem7 7452  infxpidmlem9 7454  infxpidmlem12 7457  infmap2lem1 7472  infmap2lem2 7473  alephsuc3 7478  istps4 7502  istps5 7503  isbasis2g 7505  tgval2t 7510  tgval3t 7518  tgss3t 7531  basgent 7533  clsval2 7578  elcls 7596  ntreq0 7599  islp2 7636  islpi 7638  cncnplem4 7664  sncld 7674  blrn2 7730  cncfmet 7792  metcn4 7853  fsumcnlem 7871  bcthlem7 7887  bcthlem29 7909  bcthlem32 7912  grpidinvlem3 7932  sspval 8251  isphg 8342  isph 8347  siii 8379  ishl 8457  pilem1 8503  sincosq1lem 8533  cosh111lem1 8542  cosh111lem3 8544  efifolem4 8553  effoi 8579  effoiOLD 8580  grothinf 8633  grothprimlem 8634  grothprim 8635  elghom 8651  ghomgrpilem2 8653  cayleylem2 8677  cayleylem3 8678  19.41vvvv 8695  eeeeanv 8696  r19.3rzvb 8697  ntunte 8699  ficli 8727  bsi 8739  hmeogrp 8776  subsp 8779  ishoma 8909  ismonc 8934  blkssatm 8949  avril1 8964  hvsubadd 9082  normsub0 9151  bcsALT 9195  hilcau 9217  hhcmpl 9220  hlimunii 9259  chcmh 9264  norm1ex 9273  elch0 9277  pjthlem1 9348  omlsilem 9373  pjoc2 9400  chsscon1 9514  chsscon2 9515  spanun 9596  h1deot 9601  h1det 9602  elspansn 9611  cmcm4 9669  cmbr3 9674  cmbr4 9675  osumlem5 9713  osumcor2 9721  5oalem7 9736  3oalem3 9740  pjss2 9756  mayete3 9804  cnvadj 9947  nmopunt 10068  nmcopexlem1 10080  lncnopbd 10095  nmcfnexlem1 10109  riesz2t 10128  bra11 10168  pjnmop 10200  pjssdif1 10228  pjin2 10245  pjin3 10246  pjclem1 10247  strlem1 10301  cvbr2t 10334  cvnbtwn3t 10339  cvnbtwn4t 10340  mdsl2b 10372  mdsldmd1 10380  elat2 10389  chrelat2 10414  chrelat4 10422  atoml 10431  irred 10443  mdsymlem6 10457  mdsymlem8 10459  sumdmdi 10463  dmdbr5at 10469  cdj3 10487

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