Theorem 3bitr 155

Description: A chained inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

Ref	Expression
3bitr	|- (ph <-> th)

Proof of Theorem 3bitr

Step	Hyp	Ref	Expression
1		3bitr.1	. 2 |- (ph <-> ps)
2		3bitr.2	. . 3 |- (ps <-> ch)
3		3bitr.3	. . 3 |- (ch <-> th)
4	2, 3	bitr 151	. 2 |- (ps <-> th)
5	1, 4	bitr 151	1 |- (ph <-> th)

Syntax hints:   <-> wb 127

This theorem is referenced by:  orbi1i 215  anbi1i 368  bibi2i 460  bibi1i 461  pm5.32 488  biass 511  rnlem 579  an6 638  19.43 767  excom13 776  19.12vv 960  3exdistr 970  4exdistr 971  ee4anv 982  2eu4 1070  r19.29 1295  reu2 1338  gencbvex 1372  sbralie 1439  elrabsf 1456  dfss2 1497  ss2rab 1553  symdif2 1690  dfnul2 1709  abn0 1715  disj 1733  disj4 1737  inssdif0 1754  eltp 1834  prsspw 1858  ssextss 1864  exss 1881  eqvinop 1901  uni0b 1939  unissb 1941  euuni 1954  ssint 1980  iunconst 2000  dfiun2 2014  dfiin2 2015  iunss 2017  iunrab 2022  ssiin 2024  iunn0 2029  iunxun 2035  dftr5 2044  dfwe2 2187  wereu 2197  ordtri1 2231  ordtri3 2234  onpwsuc 2315  limsuclem 2360  onzsl 2367  dfom2 2374  brinxp 2466  cbvop 2473  cnvco 2520  cnvuni 2521  dmuni 2538  dmopab2 2541  dmcosseq 2572  opelres 2579  dfima2 2604  elimasn 2617  intirr 2628  cnvsn 2636  elxp4 2640  elxp5 2641  rnuni 2646  imaiun 2650  coi1 2665  dmco2 2673  dffun2 2674  fcoi1 2765  fcoi2 2766  f1cnv 2782  f1o5 2808  f1oco 2816  fv2 2828  fnressn 2897  f1fv 2916  tz7.48lem 2993  tz7.49c 2998  elrnoprab 3054  1st2val 3097  oaord 3149  nnmord 3189  snec 3232  th3qlem1 3250  map0 3268  mapsnen 3334  xpsnen 3339  xpassen 3344  pw2en 3348  dom0 3367  fiint 3445  tz9.12lem3 3505  ranksn 3532  cp 3547  aceq5lem1 3558  aceq5lem2 3559  aceq5lem5 3562  kmlem3 3582  kmlem11 3590  kmlem12 3591  kmlem14 3593  kmlem15 3594  aceqkm 3596  cf0 3705  elni 3798  ltpiord 3809  genpn0 3900  genpass 3906  distrlem1pr 3921  psslinpr 3929  suplem1pr 3955  suplem2pr 3956  mappsrpr 4012  opelreal 4043  elreal 4044  neg11 4164  ltsubadd 4316  ltdiv23i 4412  halfpos 4421  elnn0 4536  elnn0z 4574  elznn0nn 4575  nnwos 4610  cjre 4811  negre 4825  abs00 4839  ruclem1 4885  ruclem3 4887  infxpidmlem8 4940  infxpidmlem9 4941  bcs 5101  hlimcaui 5141  choc0 5291  shlesb1 5360  chnle 5406  h1deot 5454  cmbr2 5505  pjss2 5571  pjnel 5665  large 5700

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