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 482  pm5.53 483  an42 507  pm4.11 522  ibibr 591  orddi 606  anddi 607  bibi12i 610  pm4.71r 636  pm5.18 660  nbbn 661  pm5.17 668  dfbi3 670  xor2 673  pm5.55 675  tbt 720  nbn 722  biorfi 736  orbidi 743  biluk 745  ccase 755  ccased 756  prlem2 771  rnlem 773  3orass 778  3anass 779  3ancomb 783  alex 1034  alinexa 1042  exanali 1043  alexn 1044  19.21-2 1057  19.26-2 1068  19.27 1069  19.28 1070  19.36 1078  19.37 1080  19.30 1085  19.44 1089  19.45 1090  alrot4 1097  exrot3 1099  exrot4 1100  albi 1107  2albi 1108  aaan 1119  eeor 1120  sbor 1235  sb19.21 1236  sban 1237  sbbi 1239  sblbis 1240  sbrbis 1241  sbrbif 1242  sbid2 1253  sbco2d 1256  sb8e 1262  19.23vv 1294  19.41vv 1306  19.41vvv 1307  19.42vv 1310  3exdistr 1312  4exdistr 1313  cbvex4v 1322  eeanv 1323  eeeanv 1324  sbcom2 1334  2sb5 1335  2sb6 1336  sb6a 1337  2sb5rf 1338  2sb6rf 1339  sb7f 1341  sbex 1348  sbalv 1349  exsb 1350  2exsb 1351  a12lem2 1377  euf 1384  sb8eu 1390  cbveu 1391  mo 1393  eu2 1396  mo2 1400  mo3 1401  mo4f 1402  eu4 1410  moanim 1427  euan 1428  mopick2 1436  2exeu 1446  2mo 1447  2mos 1448  2eu1 1449  2eu3 1451  2eu4 1452  2eu6 1454  exists1 1457  abid 1465  eqeq12i 1488  eleq12i 1539  abeq2 1568  abeq2i 1570  eq2ab 1573  clabel 1582  sbabel 1584  necon3abii 1596  necon1abii 1616  neanior 1639  ralinexa 1683  rexanali 1684  r3al 1690  r19.26 1750  r19.26-2 1751  r19.43 1765  ralcom 1774  rexcom 1775  ralcom2 1776  reeanv 1778  cbvral2v 1803  cbvral3v 1804  rabeq2i 1810  ceqsex2 1836  vtocl2 1843  vtocl3 1844  vtoclgf 1846  cla4gf 1860  cla43gv 1867  eqvincf 1884  ceqsrex2v 1890  elrab2 1907  euxfr2 1926  euxfr 1927  reu2 1930  rmo4 1933  reu4 1934  reu7 1935  2reuswap 1937  sbralie 1941  sbccomglem 1988  ra5 2000  dfss 2054  ss2ab 2116  dfpss2 2133  psseq12i 2139  pssn2lp 2147  sspsstri 2148  uneqri 2174  ssequn2 2203  unss 2204  ineqri 2209  sseqin2 2229  nssinpss 2240  nsspssun 2241  dfss4 2242  difin 2245  symdif2 2266  inrab2 2272  reuun2 2278  rab0 2293  eq0 2294  0el 2296  0pss 2308  npss0 2309  disj1 2312  disjpss 2319  undif4 2325  difin0ss 2332  inssdif0 2333  r19.3rzv 2348  ralidm 2357  dfpr2 2422  ralpr 2428  rexpr 2429  eusn 2446  eldifsn 2462  difprsn 2465  pw0 2468  pwpw0 2469  eqsn 2474  prsspw 2480  prel12 2484  preqsn 2486  pwsnALT 2501  eluniab 2513  elunirab 2514  unipr 2515  uniun 2519  uniin 2520  unissb 2528  elintab 2544  elintrab 2545  ssintab 2550  intun 2562  intpr 2563  iuniin 2573  iuneq2 2578  dfiun2g 2586  dfiin2 2588  iunss 2591  iunid 2603  iun0 2604  0iun 2605  iunxsn 2612  iunun 2613  iunxun 2614  iununi 2616  iunpwss 2618  inex1 2716  pwex 2745  pwssb 2760  exss 2769  dtru 2772  zfpair2 2780  elop 2783  copsexg 2792  opeqsn 2802  opthwiener 2807  opabid 2810  brabg 2818  opabn0 2824  pwunss 2826  pwundif 2828  dfid3 2836  pocl 2844  sotric 2860  so 2864  uniuni 2880  reuxfr2 2903  reuxfr 2904  elpwun 2911  iunpw 2914  dffr2 2919  fr3nr 2926  dfepfr 2932  dfwe2 2935  wefrc 2943  ordtri3or 2979  ordtri2 2982  onintrab2 3014  elsuci 3035  elsucg 3036  sucel 3042  sucid 3051  ordtri2or 3077  ordzsl 3116  onzsl 3117  dflim4 3119  on0eqelt 3124  snsn0non 3125  findsg 3157  tfindsg 3162  elxp 3202  opelxp 3214  brxp 3215  rexxp 3219  ralxpf 3220  opthprc 3221  xpundi 3225  xpundir 3226  xp0r 3239  reluni 3265  relop 3275  opelco 3288  brco 3289  elcnv 3293  elcnv2 3294  eldm2 3308  dmun 3317  dmin 3318  dmi 3326  dmcoss 3363  dmcosseq 3365  rncoeq 3367  resiexg 3396  dfima3 3406  elima2 3409  elima3 3410  imai 3417  imasng 3424  cotr 3436  cnvsym 3437  asymref 3439  asymref2 3440  intirr 3441  cnvopab 3445  cnvsn 3449  elxp4 3453  elxp5 3454  imainss 3463  cnvxp 3464  dfrel2 3485  dfrel3 3489  cores 3499  imaco 3501  coi1 3510  coass 3512  relssdr 3513  cnvpo 3522  dffun2 3526  dffun3 3527  dffun4 3528  dffun5 3529  dffun6 3539  dffun8 3541  funopab 3548  funun 3554  funcnv 3557  fun2cnv 3559  fncnv 3561  fun11 3562  fununi 3563  funcnvuni 3564  imadif 3574  funimaexg 3575  isarep1 3577  fnopabg 3615  fnopab2g 3616  fun 3641  fcoi1 3645  fcoi2 3646  fcnvres 3648  fconst 3658  f11 3664  funforn 3678  f1o2 3693  f1ocnv 3701  ffoss 3711  f11o 3712  f1o00 3714  fo00 3715  fv2 3720  elfv 3722  fv3 3733  tz6.12-1 3736  nfvres 3748  fvopab5 3793  dff3 3818  dffo3 3819  dffo5 3821  ffnfvf 3829  fopabfv 3831  fsn2 3836  fconst3 3850  fconst4 3851  funfvima 3852  imaiun 3864  abexssex 3872  f1fv 3874  f1fvf 3875  isoini 3900  tfrlem3 3913  tfrlem7 3917  tfrlem9 3919  dfrdg2 3933  tz7.48lem 3955  tz7.48-2 3957  dfoprab2 3991  dmoprab 4002  rnoprab 4004  resoprab 4009  ffnoprval 4014  fnoprval 4017  foprval 4018  oprabex3 4022  oprabval3 4030  oprabval6g 4032  fooprval 4037  ndmoprdistr 4049  1st2val 4095  2nd2val 4096  2ndconst 4097  curry1 4098  dfopab2 4113  dfoprab3 4114  dfoprab5 4115  foprab2 4119  el1o 4146  oarec 4196  oeordi 4214  oaabs 4252  dfer2 4262  eqerlem 4270  erdisj 4286  elqs 4290  ecid 4300  qsid 4301  brecop 4306  ecopoprsym 4310  th3qlem1 4314  mapval2 4335  elpm 4336  elpm2 4337  mapsn 4345  ixpeq2 4355  domen 4379  isfi 4382  en1 4426  2dom 4427  xpsnen 4435  xpcomen 4439  xpassen 4441  pw2en 4446  sbthlem9 4455  sdomdomtr 4469  pwuninel 4486  2pwuninel 4487  xpen 4488  mapxpen 4495  xpmapenlem5 4500  ssenen 4504  nneneq 4512  php 4513  0sdom1dom 4525  unfilem1 4548  abfii2OLD 4562  abfii4OLD 4564  iunfiOLD 4569  supmo 4576  zfreg2 4597  inf2 4608  inf3lem2 4614  axinf2 4624  zfinf 4626  trcl 4645  zfregs 4647  setind2 4649  tz9.12lem1 4659  tz9.12lem3 4661  rankel 4680  rankval3 4681  unbndrank 4683  rankun 4691  scottexs 4718  scott0s 4719  cplem1 4720  bnd2 4724  kardex 4725  karden 4726  aceq1 4729  aceq2 4731  aceq3lem 4732  aceq3 4733  aceq4 4734  aceq5lem1 4735  aceq5lem2 4736  aceq5lem3 4737  aceq5lem4 4738  aceq5lem5 4739  aceq6b 4742  ac6n 4757  ac9s 4764  kmlem3 4767  kmlem4 4768  kmlem7 4771  kmlem8 4772  kmlem9 4773  kmlem13 4777  kmlem14 4778  kmlem15 4779  aceqkm 4781  zorn2lem6 4793  brdom7disj 4804  brdom6disj 4805  card1 4833  sucxpdom 4846  iscard 4853  iscard2 4854  alephord2 4876  alephislim 4883  cardaleph 4885  alephval3 4903  cf0 4910  cfeq0 4914  cfsuc 4915  cdaen 4924  cdadom1 4933  elni 5004  ltexpi 5029  ltsopq 5075  genpv 5102  genpn0 5106  genpass 5112  1pr 5117  addcompr 5123  mulcompr 5125  distrlem1pr 5127  distrlem5pr 5131  prlem934b 5138  reclem1pr 5156  reclem2pr 5157  suplem1pr 5161  ltsosr 5203  ltasr 5209  mappsrpr 5218  map2psrpr 5220  suppsr3 5224  opelcn 5248  elreal 5250  axaddopr 5265  axmulopr 5266  axicn 5270  axrnegex 5283  axrrecex 5284  pre-axmulgt0 5290  pre-axsup 5291  subadd2 5373  neg11 5406  1re 5435  ltxrltt 5500  xrlenltt 5501  leloet 5518  xrleloet 5557  xrrebndt 5568  ltadd1 5591  leadd2 5593  addgt0 5598  ltneg 5603  ltnegcon2 5605  msqgt0 5613  msq0 5695  rec11i 5777  divmul24t 5783  halfpos 5904  infm3 6054  infmsup 6068  arch 6071  xrinfmss 6079  supxrre 6083  elnnz 6145  elznn0nn 6148  elznn0 6149  elznn 6150  elnn0nn 6171  elnnnn0 6172  zltp1let 6181  uzwo3 6218  zmin 6219  elq 6257  ralrp 6289  icounlem 6412  snunioolem 6414  raluz2 6443  rexuz2 6445  nnwof 6459  nnwos 6460  subsq0 6648  nn0le2msqt 6663  nn0opth2 6667  inelr 6735  replimt 6761  abslt 6875  absle 6876  cau4i 6918  cau5 6919  cvg3 6923  bcpasc 6969  dffsum 6998  csbfsum 7027  clm4 7080  climunii 7098  climeu 7100  climshft2 7106  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  mulc1cncf 7279  ef1tllem 7381  eirrlem1 7389  ruclem1 7510  ruclem3 7512  ruclem8 7517  infxpidmlem6 7557  infxpidmlem7 7558  infxpidmlem9 7560  infxpidmlem12 7563  infmap2lem1 7579  infmap2lem2 7580  alephsuc3 7585  istps4OLD 7609  istps5OLD 7610  isbasis2g 7612  tgval2t 7617  tgval3t 7625  tgss3t 7638  basgent 7640  clsval2 7685  elcls 7704  ntreq0 7708  islp2 7747  islpi 7749  cncnplem4 7777  sncld 7787  blrn2 7842  cncfmet 7905  metcn4 7971  fsumcnlem 7989  bcthlem7 8005  bcthlem29 8027  bcthlem32 8030  grpidinvlem3 8050  sspval 8382  isphg 8476  isph 8481  siii 8513  ishl 8591  spwmo 8656  spwpr2 8658  pilem1 8671  sincosq1lem 8703  cosh111lem1 8714  cosh111lem3 8716  efifolem4 8725  effoi 8745  grothinf 8781  grothprimlem 8782  grothprim 8783  avril1 8784  h2hcau 8849  axhcompl 8868  hvsubadd 8933  normsub0 9002  bcsALT 9046  hhcmpl 9069  hlimunii 9108  chcmh 9113  norm1ex 9122  elch0 9126  hhsssh2 9140  pjthlem1 9219  omlsilem 9244  pjoc2 9271  chsscon1 9385  chsscon2 9386  spanun 9467  h1deot 9472  h1det 9473  elspansn 9481  cmcm4 9538  cmbr3 9543  cmbr4 9544  osumlem5 9582  osumcor2 9590  5oalem7 9605  3oalem3 9609  pjss2 9625  mayete3 9673  cnvadj 9816  nmopunt 9939  nmcopexlem1 9951  lncnopbd 9966  nmcfnexlem1 9980  riesz2t 9999  nmopcoadj0 10036  bra11 10041  pjnmop 10075  pjssdif1 10103  pjin2 10121  pjin3 10122  pjclem1 10123  strlem1 10177  cvbr2t 10210  cvnbtwn3t 10215  cvnbtwn4t 10216  mdsl2b 10250  mdsldmd1 10258  elat2 10267  chrelat2 10292  chrelat4 10300  atoml 10309  irred 10321  mdsymlem6 10335  mdsymlem8 10337  sumdmdi 10342  dmdbr5at 10349  cdj3 10368  elghom 10384  ghomgrpilem2 10386  cayleylem2 10410  cayleylem3 10411  19.41vvvv 10435  eeeeanv 10436  r19.3rzvb 10437  ntunte 10439  ficli 10472  ficliOLD 10473  bsi 10495  hmeogrp 10538  subsp 10554  rcfpfillem2 10587  rcfpfillem2OLD 10588  ishoma 10715  ismonc 10742  blkssatm 10767

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