Theorem bitr 151

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 133	. . 3 |- (ph -> ps)
3		bitr.2	. . . 4 |- (ps <-> ch)
4	3	biimp 133	. . 3 |- (ps -> ch)
5	2, 4	syl 12	. 2 |- (ph -> ch)
6	3	biimpr 134	. . 3 |- (ch -> ps)
7	1	biimpr 134	. . 3 |- (ps -> ph)
8	6, 7	syl 12	. 2 |- (ch -> ph)
9	5, 8	impbi 139	1 |- (ph <-> ch)

Syntax hints:   <-> wb 127

This theorem is referenced by:  bitr2 152  bitr3 153  bitr4 154  3bitr 155  3bitr3 156  3bitr4 158  imbi12i 163  dfor2 199  iman 205  orbi12i 216  or42 221  anor 252  oran 255  impexp 276  anass 336  anbi12i 369  an42 389  pm4.11 400  orddi 458  anddi 459  bibi12i 462  pm4.71r 482  oibabs 493  pm5.18 497  nbbn 498  dfbi 499  orbidi 510  biass 511  biluk 512  biorfi 552  caselem 561  prlem2 577  rnlem 579  3orass 584  3anass 585  3ancomb 589  alex 717  alinexa 724  exanali 725  alexn 726  19.30 764  exrot3 777  exrot4 778  albi 785  aaan 794  eeor 795  sbor 887  sb19.21 888  sban 889  sbbi 890  sblbis 891  sbrbis 892  sbrbif 893  sbid2 911  sbco2d 914  sb8e 919  19.23vv 951  19.41vv 964  19.41vvv 965  19.42vv 968  3exdistr 970  4exdistr 971  cbvex4v 979  eeanv 980  eeeanv 981  sb6a 990  sbcom2 992  sbex 998  sbalv 999  euf 1011  sb8eu 1017  cbveu 1018  mo 1020  eu2 1023  mo2 1026  mo3 1027  mo4f 1028  eu4 1036  moanim 1051  euanv 1053  mopick2 1057  2exeu 1066  2eu1 1067  2eu3 1069  2eu4 1070  exists1 1072  abid 1094  cleq12i 1114  eleq12i 1154  cleqab 1174  cleqabi 1176  cleq2ab 1179  sbabel 1189  r3al 1240  r19.21v 1260  r19.26 1289  r19.26-2 1290  r19.43 1304  ralcom 1312  rexcom 1313  ralcom2 1314  reeanv 1316  cbvral2v 1336  reu2 1338  reu4 1340  2reuswap 1341  cleqrabi 1347  vtocl2 1379  vtocl3 1380  vtoclgf 1382  cla4gf 1394  eqvincf 1408  euxfr2 1435  euxfr 1436  sbralie 1439  rax5 1472  dfss 1493  sseq12i 1526  ss2ab 1551  dfpss2 1557  psseq12i 1563  pssn2lp 1571  sspsstri 1572  reuxfr2 1579  reuxfr 1580  uneqri 1602  ssequn2 1631  unss 1632  ineqri 1637  sseqin2 1656  nssinpss 1665  nsspssun 1666  dfss4 1667  difin 1670  symdif2 1690  inex1 1697  rab0 1718  eq0 1719  0el 1720  0pss 1730  disjpss 1738  undif4 1744  difin0ss 1753  inssdif0 1754  r19.3rzv 1767  ralidm 1774  pwex 1806  dfpr2 1821  prsspw 1858  prel12 1875  exss 1881  pwpw0 1883  dtru 1889  elop 1894  copsexg 1902  eusn 1913  opthwiener 1914  pwunss 1916  eluniab 1926  unpr 1930  uniun 1934  uniin 1935  unissb 1941  elintab 1976  elintrab 1977  intun 1989  intpr 1990  iuniin 2001  iuneq2 2006  dfiun2 2014  dfiin2 2015  iunss 2017  ssiin 2024  iun0 2028  iunxsn 2034  iunxun 2035  iununi 2037  iunpwss 2039  iunpw 2040  dftr5 2044  dftr3 2045  breq12i 2070  opabid 2099  brabg 2116  pocl 2132  sotric 2148  so 2152  supmo 2156  dffr2 2171  dfepfr 2184  dfwe2 2187  wefrc 2195  ordsseleq 2227  ordtri3or 2230  ordtri2 2233  onintrab2 2269  elsuci 2289  elsucg 2290  sucel 2296  sucid 2304  onmindif2 2313  ordtri2or 2328  ordzsl 2366  onzsl 2367  on0eqelt 2370  snsn0non 2371  elxp 2442  opelxp 2452  brxp 2453  opthprc 2457  xpundi 2461  xpundir 2462  xp0r 2474  cleqrel 2483  reluni 2493  opelco 2509  brco 2510  elcnv 2514  elcnv2 2515  eldm2 2528  dmun 2536  dmin 2537  dmi 2545  reldm0 2550  dmco 2570  dmcosseq 2572  rncoeq 2574  dfima3 2605  elima2 2607  elima3 2608  imai 2613  eliniseg 2618  cotr 2625  cnvsym 2626  intirr 2628  cnvopab 2632  cnvsn 2636  elxp4 2640  elxp5 2641  imainss 2649  imaiun 2650  cnvxp 2651  cores 2659  dfrel2 2660  coi1 2665  coass 2667  relssdr 2668  dmco2 2673  dffun2 2674  dffun3 2675  dffun4 2676  dffun5 2677  dffun6 2687  funopab 2694  funun 2700  funcnv2 2702  funcnv 2703  fun2cnv 2704  fununi 2705  funcnvuni 2706  imadif 2714  funimaexg 2715  fnopabg 2745  fun 2763  fcoi1 2765  fcoi2 2766  fcnvres 2768  fconst 2774  f11 2780  funforn 2792  f1o2 2804  f1ocnv 2811  f1oco 2816  ffoss 2820  f11o 2821  f1o00 2823  fv2 2828  elfv 2830  fv3 2839  tz6.12-1 2842  nfvres 2850  fvopabn 2873  elrnopab 2884  fopabfv 2894  fsn 2895  fsn2 2896  funfvima 2904  f1fv 2916  f1fvf 2917  isoini 2938  tfrlem3 2951  tfrlem7 2955  tfrlem8 2956  tfrlem9 2957  tz7.48lem 2993  tz7.48-2 2995  dfoprab2 3021  dmoprab 3031  rnoprab 3033  fnoprab2 3039  ffnoprval 3041  fnoprval 3042  foprval 3043  oprabex3 3046  oprabval3 3052  elrnoprab 3054  ndmoprdistr 3063  1st2val 3097  el1o 3115  oawordeulem 3156  er2 3201  erdisj 3223  elqs 3227  ecid 3236  qsid 3237  brecop 3242  ecopoprsym 3246  th3qlem1 3250  elmap 3265  mapsn 3269  domen 3284  en1 3331  2dom 3332  mapsnen 3334  map1 3335  xpsnen 3339  xpcomen 3343  xpassen 3344  pw2en 3348  sbthlem9 3357  0sdom 3368  sdomdomtr 3370  xpen 3383  mapxpen 3390  xpmapenlem5 3395  ssenen 3399  nneneq 3408  0sdom1dom 3420  unfilem1 3438  zfreg2 3448  inf2 3459  inf3lema 3460  inf3lem2 3465  inf4 3473  zfinf 3474  trcl 3489  zfregs 3491  setind2 3493  tz9.12lem1 3503  tz9.12lem3 3505  rankel 3524  rankval3 3525  unbndrank 3527  rankun 3535  scottexs 3543  scott0s 3544  cplem1 3545  bnd2 3549  kardex 3550  karden 3551  aceq1 3552  aceq2 3554  aceq3lem 3555  aceq3 3556  aceq4 3557  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  aceq5lem4 3561  aceq5lem5 3562  aceq6b 3565  kmlem3 3582  kmlem4 3583  kmlem7 3586  kmlem8 3587  kmlem11 3590  kmlem12 3591  kmlem13 3592  kmlem14 3593  kmlem15 3594  kmlem16 3595  aceqkm 3596  zornlem2 3604  zornlem6 3608  fodomb 3615  sucxpdom 3652  iscard 3659  iscard2 3660  alephord2 3681  alephislim 3688  cardaleph 3690  cf0 3705  cfsuc 3709  cdaen 3719  cdadom1 3727  ltexpi 3823  ltsopq 3869  genpv 3896  genpn0 3900  genpass 3906  1pr 3911  addcompr 3917  mulcompr 3919  distrlem1pr 3921  distrlem5pr 3925  prlem934b 3932  reclem1pr 3950  reclem2pr 3951  suplem1pr 3955  ltsosr 3997  ltasr 4003  mappsrpr 4012  map2psrpr 4014  suppsr3 4018  opelcn 4042  elreal 4044  axicn 4065  axrecex 4079  axrnegex 4080  axrrecex 4081  axmulgt0 4086  axsup 4088  addcan2 4121  neg11 4164  sq0 4211  rec11i 4261  leltt 4278  leloet 4284  ltadd1 4313  leadd2 4315  ltsubadd2 4317  lesubadd2 4318  lesubadd 4319  addgt0 4323  ltaddpos 4327  ltneg 4330  ltnegcon1 4332  ltnegcon2 4333  lesub0 4341  sqgt0 4343  ltdiv23i 4412  halfpos 4421  arch 4521  inelr 4527  elz 4565  elnnz 4572  elznn0nn 4575  elznn0 4576  elnn0nn 4593  elnnnn0 4594  zltp1let 4597  nnwof 4609  nnwos 4610  uzwo3lem2 4615  uzwo3 4616  zmin 4617  elq 4629  sqe0 4687  nn0le2sqet 4721  nn0opth2 4725  sqrlem4 4734  replimt 4798  absgt0 4842  absnid 4851  climunii 4883  ruclem1 4885  ruclem2 4886  ruclem3 4887  ruclem8 4892  infxpidmlem6 4938  infxpidmlem7 4939  infxpidmlem9 4941  infxpidmlem12 4944  infmap2lem1 4951  infmap2lem2 4952  alephsuc3 4955  hvsubadd 5038  normsub0 5084  bcs 5101  hlimunii 5143  chcmh 5148  elch0 5158  projlem8 5200  projlem10 5202  projlem13 5205  projlem15 5207  pjthlem1 5225  pjthu 5241  pjthu2 5242  omlsilem 5249  pjoc2 5273  shne0 5372  chsscon1 5384  chsscon2 5385  spanun 5450  h1deot 5454  h1det 5455  h1de2b 5459  h1de2ctlem 5460  elspansn 5463  cmcm4 5504  cmbr2 5505  cmbr3 5509  cmbr4 5510  osumlem5 5534  5oalem7 5550  3oalem3 5554  pjss2 5571  pjin2 5647  pjin3 5648  pjclem1 5649  strlem1 5691  cvbr2t 5715  cvnbtwn3t 5720  cvnbtwn4t 5721  elat 5738  elat2 5739  atom1d 5750  chrelat2 5758  mdsymlem6 5781  mdsymlem8 5783  sumdmdi 5785

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

This theorem depends on definitions:  df-bi 128

metamath.org