HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 bitr.1 . . . 4 |- (ph <-> ps)
21biimp 151 . . 3 |- (ph -> ps)
3 bitr.2 . . . 4 |- (ps <-> ch)
43biimp 151 . . 3 |- (ps -> ch)
52, 4syl 10 . 2 |- (ph -> ch)
63biimpr 152 . . 3 |- (ch -> ps)
71biimpr 152 . . 3 |- (ps -> ph)
86, 7syl 10 . 2 |- (ch -> ph)
95, 8impbi 157 1 |- (ph <-> ch)
Colors of variables: wff set class
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 521  ibibr 590  orddi 605  anddi 606  bibi12i 609  pm4.71r 635  pm5.18 659  nbbn 660  pm5.17 667  dfbi 669  xor2 672  pm5.55 674  tbt 719  nbn 721  biorfi 735  orbidi 742  biluk 744  ccase 754  ccased 755  prlem2 770  rnlem 772  3orass 777  3anass 778  3ancomb 782  alex 1032  alinexa 1040  exanali 1041  alexn 1042  19.21-2 1055  19.26-2 1066  19.27 1067  19.28 1068  19.36 1076  19.37 1078  19.30 1083  19.44 1087  19.45 1088  alrot4 1095  exrot3 1097  exrot4 1098  albi 1105  2albi 1106  aaan 1117  eeor 1118  sbor 1233  sb19.21 1234  sban 1235  sbbi 1237  sblbis 1238  sbrbis 1239  sbrbif 1240  sbid2 1251  sbco2d 1254  sb8e 1260  19.23vv 1292  19.41vv 1304  19.41vvv 1305  19.42vv 1308  3exdistr 1310  4exdistr 1311  cbvex4v 1320  eeanv 1321  eeeanv 1322  sbcom2 1332  2sb5 1333  2sb6 1334  sb6a 1335  2sb5rf 1336  2sb6rf 1337  sb7f 1339  sbex 1346  sbalv 1347  exsb 1348  2exsb 1349  a12lem2 1375  euf 1382  sb8eu 1388  cbveu 1389  mo 1391  eu2 1394  mo2 1398  mo3 1399  mo4f 1400  eu4 1408  moanim 1425  euan 1426  mopick2 1434  2exeu 1444  2mo 1445  2mos 1446  2eu1 1447  2eu3 1449  2eu4 1450  2eu6 1452  exists1 1455  abid 1463  eqeq12i 1485  eleq12i 1536  abeq2 1565  abeq2i 1567  eq2ab 1570  clabel 1579  sbabel 1581  necon3abii 1593  necon1abii 1613  neanior 1636  ralinexa 1680  rexanali 1681  r3al 1687  r19.26 1747  r19.26-2 1748  r19.43 1762  ralcom 1771  rexcom 1772  ralcom2 1773  reeanv 1775  cbvral2v 1799  cbvral3v 1800  rabeq2i 1806  ceqsex2 1832  vtocl2 1839  vtocl3 1840  vtoclgf 1842  cla4gf 1856  cla43gv 1863  eqvincf 1880  ceqsrex2v 1886  elrab2 1903  euxfr2 1922  euxfr 1923  reu2 1926  rmo4 1929  reu4 1930  reu7 1931  2reuswap 1933  sbralie 1937  sbccomglem 1984  ra5 1996  dfss 2050  ss2ab 2112  dfpss2 2129  psseq12i 2135  pssn2lp 2143  sspsstri 2144  uneqri 2170  ssequn2 2199  unss 2200  ineqri 2205  sseqin2 2225  nssinpss 2236  nsspssun 2237  dfss4 2238  difin 2241  symdif2 2262  inrab2 2268  reuun2 2274  rab0 2289  eq0 2290  0el 2292  0pss 2304  npss0 2305  disj1 2308  disjpss 2315  undif4 2321  difin0ss 2328  inssdif0 2329  r19.3rzv 2344  ralidm 2353  dfpr2 2418  ralpr 2424  rexpr 2425  eusn 2442  eldifsn 2458  difprsn 2461  pw0 2464  pwpw0 2465  eqsn 2470  prsspw 2476  prel12 2480  preqsn 2482  eluniab 2508  elunirab 2509  unipr 2510  uniun 2514  uniin 2515  unissb 2523  elintab 2539  elintrab 2540  ssintab 2545  intun 2557  intpr 2558  iuniin 2568  iuneq2 2573  dfiun2g 2581  dfiin2 2583  iunss 2586  iunid 2598  iun0 2599  0iun 2600  iunxsn 2607  iunun 2608  iunxun 2609  iununi 2611  iunpwss 2613  inex1 2711  pwex 2740  pwssb 2755  exss 2764  dtru 2767  zfpair2 2775  elop 2778  copsexg 2787  opeqsn 2797  opthwiener 2802  opabid 2805  brabg 2813  opabn0 2819  pwunss 2821  pwundif 2823  dfid3 2831  pocl 2839  sotric 2855  so 2859  uniuni 2875  reuxfr2 2898  reuxfr 2899  elpwun 2906  iunpw 2909  dffr2 2914  fr3nr 2921  dfepfr 2927  dfwe2 2930  wefrc 2938  ordtri3or 2974  ordtri2 2977  onintrab2 3009  elsuci 3030  elsucg 3031  sucel 3037  sucid 3046  ordtri2or 3072  ordzsl 3111  onzsl 3112  dflim4 3114  on0eqelt 3119  snsn0non 3120  findsg 3152  tfindsg 3157  elxp 3197  opelxp 3209  brxp 3210  rexxp 3214  ralxpf 3215  opthprc 3216  xpundi 3220  xpundir 3221  xp0r 3234  reluni 3260  relop 3270  opelco 3283  brco 3284  elcnv 3288  elcnv2 3289  eldm2 3303  dmun 3312  dmin 3313  dmi 3321  dmcoss 3355  dmcosseq 3357  rncoeq 3359  resiexg 3388  dfima3 3398  elima2 3401  elima3 3402  imai 3409  imasng 3416  cotr 3428  cnvsym 3429  asymref 3431  asymref2 3432  intirr 3433  cnvopab 3437  cnvsn 3441  elxp4 3445  elxp5 3446  imainss 3455  cnvxp 3456  dfrel2 3477  dfrel3 3481  cores 3491  imaco 3493  coi1 3502  coass 3504  relssdr 3505  cnvpo 3514  dffun2 3518  dffun3 3519  dffun4 3520  dffun5 3521  dffun6 3531  dffun8 3533  funopab 3540  funun 3546  funcnv 3549  fun2cnv 3551  fncnv 3553  fun11 3554  fununi 3555  funcnvuni 3556  imadif 3566  funimaexg 3567  isarep1 3569  fnopabg 3607  fnopab2g 3608  fun 3632  fcoi1 3636  fcoi2 3637  fcnvres 3639  fconst 3649  f11 3655  funforn 3669  f1o2 3684  f1ocnv 3692  ffoss 3702  f11o 3703  f1o00 3705  fo00 3706  fv2 3711  elfv 3713  fv3 3724  tz6.12-1 3727  nfvres 3739  fvopab5 3784  dff3 3809  dffo3 3810  dffo5 3812  ffnfvf 3820  fopabfv 3822  fsn2 3827  fconst3 3841  fconst4 3842  funfvima 3843  imaiun 3855  abexssex 3863  f1fv 3865  f1fvf 3866  isoini 3891  tfrlem3 3904  tfrlem7 3908  tfrlem9 3910  dfrdg2 3924  tz7.48lem 3946  tz7.48-2 3948  dfoprab2 3982  dmoprab 3993  rnoprab 3995  resoprab 4000  ffnoprval 4005  fnoprval 4008  foprval 4009  oprabex3 4013  oprabval3 4021  oprabval6g 4023  fooprval 4028  ndmoprdistr 4041  1st2val 4085  2nd2val 4086  2ndconst 4087  curry1 4088  dfopab2 4103  dfoprab3 4104  dfoprab5 4105  foprab2 4109  el1o 4136  oarec 4186  oeordi 4204  oaabs 4242  dfer2 4252  eqerlem 4260  erdisj 4276  elqs 4280  ecid 4290  qsid 4291  brecop 4296  ecopoprsym 4300  th3qlem1 4304  mapval2 4325  elpm 4326  elpm2 4327  mapsn 4335  ixpeq2 4345  domen 4367  en1 4413  2dom 4414  xpsnen 4421  xpcomen 4425  xpassen 4427  pw2en 4432  sbthlem9 4441  sdomdomtr 4455  pwuninel 4472  2pwuninel 4473  xpen 4474  mapxpen 4481  xpmapenlem5 4486  ssenen 4490  nneneq 4498  php 4499  0sdom1dom 4510  unfilem1 4530  abfii2 4542  abfii4 4544  iunfi 4549  supmo 4556  zfreg2 4577  inf2 4588  inf3lem2 4594  axinf2 4604  zfinf 4606  trcl 4625  zfregs 4627  setind2 4629  tz9.12lem1 4639  tz9.12lem3 4641  rankel 4660  rankval3 4661  unbndrank 4663  rankun 4671  scottexs 4698  scott0s 4699  cplem1 4700  bnd2 4704  kardex 4705  karden 4706  aceq1 4709  aceq2 4711  aceq3lem 4712  aceq3 4713  aceq4 4714  aceq5lem1 4715  aceq5lem2 4716  aceq5lem3 4717  aceq5lem4 4718  aceq5lem5 4719  aceq6b 4722  ac6n 4737  ac9s 4744  kmlem3 4747  kmlem4 4748  kmlem7 4751  kmlem8 4752  kmlem9 4753  kmlem13 4757  kmlem14 4758  kmlem15 4759  aceqkm 4761  zorn2lem6 4773  brdom7disj 4784  brdom6disj 4785  card1 4813  sucxpdom 4826  iscard 4833  iscard2 4834  alephord2 4856  alephislim 4863  cardaleph 4865  alephval3 4883  cf0 4890  cfeq0 4894  cfsuc 4895  cdaen 4904  cdadom1 4913  elni 4984  ltexpi 5009  ltsopq 5055  genpv 5082  genpn0 5086  genpass 5092  1pr 5097  addcompr 5103  mulcompr 5105  distrlem1pr 5107  distrlem5pr 5111  prlem934b 5118  reclem1pr 5136  reclem2pr 5137  suplem1pr 5141  ltsosr 5183  ltasr 5189  mappsrpr 5198  map2psrpr 5200  suppsr3 5204  opelcn 5228  elreal 5230  axaddopr 5245  axmulopr 5246  axicn 5250  axrnegex 5263  axrrecex 5264  pre-axmulgt0 5270  pre-axsup 5271  subadd2 5353  neg11 5386  1re 5415  ltxrltt 5480  xrlenltt 5481  leloet 5499  xrleloet 5538  xrrebndt 5549  ltadd1 5573  leadd2 5575  addgt0 5580  ltneg 5585  ltnegcon2 5587  msqgt0 5595  msq0 5672  rec11i 5741  divmul24t 5747  halfpos 5860  infm3 6009  infmsup 6023  arch 6026  xrinfmss 6034  supxrre 6038  elnnz 6100  elznn0nn 6103  elznn0 6104  elznn 6105  elnn0nn 6126  elnnnn0 6127  zltp1let 6136  uzwo3 6174  zmin 6175  elq 6203  ralrp 6234  icounlem 6353  snunioolem 6355  raluz2 6383  rexuz2 6385  nnwof 6399  nnwos 6400  sq00 6554  subsq0 6587  nn0le2msqt 6601  nn0opth2 6605  inelr 6673  replimt 6700  abslt 6818  absle 6819  cau4i 6863  cau5 6864  cvg3 6868  bcpasc 6915  dffsum 6944  csbfsum 6973  clm4 7026  climunii 7043  climeu 7045  climshft2 7051  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  mulc1cncf 7222  ef1tllem 7331  eirrlem1 7338  ruclem1 7461  ruclem3 7463  ruclem8 7468  infxpidmlem6 7508  infxpidmlem7 7509  infxpidmlem9 7511  infxpidmlem12 7514  infmap2lem1 7529  infmap2lem2 7530  alephsuc3 7535  istps4 7559  istps5 7560  isbasis2g 7562  tgval2t 7567  tgval3t 7575  tgss3t 7588  basgent 7590  clsval2 7635  elcls 7654  ntreq0 7658  islp2 7697  islpi 7699  cncnplem4 7727  sncld 7737  blrn2 7794  cncfmet 7857  metcn4 7921  fsumcnlem 7939  bcthlem7 7955  bcthlem29 7977  bcthlem32 7980  grpidinvlem3 8000  sspval 8329  isphg 8420  isph 8425  siii 8457  ishl 8535  spwmo 8598  pilem1 8609  sincosq1lem 8639  cosh111lem1 8648  cosh111lem3 8650  efifolem4 8659  effoi 8684  grothinf 8720  grothprimlem 8721  grothprim 8722  avril1 8723  h2hcau 8788  axhcompl 8807  hvsubadd 8872  normsub0 8941  bcsALT 8985  hhcmpl 9008  hlimunii 9047  chcmh 9052  norm1ex 9061  elch0 9065  hhsssh2 9079  pjthlem1 9157  omlsilem 9182  pjoc2 9209  chsscon1 9323  chsscon2 9324  spanun 9405  h1deot 9410  h1det 9411  elspansn 9420  cmcm4 9478  cmbr3 9483  cmbr4 9484  osumlem5 9522  osumcor2 9530  5oalem7 9545  3oalem3 9549  pjss2 9565  mayete3 9613  cnvadj 9756  nmopunt 9877  nmcopexlem1 9889  lncnopbd 9904  nmcfnexlem1 9918  riesz2t 9937  nmopcoadj0 9974  bra11 9979  pjnmop 10013  pjssdif1 10041  pjin2 10059  pjin3 10060  pjclem1 10061  strlem1 10115  cvbr2t 10148  cvnbtwn3t 10153  cvnbtwn4t 10154  mdsl2b 10187  mdsldmd1 10195  elat2 10204  chrelat2 10229  chrelat4 10237  atoml 10246  irred 10258  mdsymlem6 10272  mdsymlem8 10274  sumdmdi 10278  dmdbr5at 10284  cdj3 10302  elghom 10318  ghomgrpilem2 10320  cayleylem2 10344  cayleylem3 10345  19.41vvvv 10371  eeeeanv 10372  r19.3rzvb 10373  ntunte 10376  ficli 10404  bsi 10418  hmeogrp 10461  subsp 10465  ishoma 10595  ismonc 10620  blkssatm 10639
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