Theorem bitr4 154

Description: An inference from transitive law for logical equivalence.

Hypotheses

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

Assertion

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

Proof of Theorem bitr4

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

Syntax hints:   <-> wb 127

This theorem is referenced by:  3bitr4 158  3bitr4r 159  imor 204  oridm 208  ianor 253  ioran 254  bi 396  bibi2i 460  pm5.32 488  orcana 509  mpbiran 547  mpbiranr 548  prlem2 577  3anrev 590  an6 638  19.27 750  19.28 751  19.36 757  19.37 759  19.44 768  19.45 769  19.33b 771  19.41 774  eqsal 833  sb5y 883  sbequ8 902  hbsb4t 906  sbel2x 995  eu2 1023  eu3 1024  eu5 1035  moanim 1051  euanv 1053  2eu4 1070  2eu5 1071  cleqf 1167  sbabel 1189  r2al 1231  r2ex 1241  r19.23v 1282  r19.26m 1291  r19.27av 1293  r19.29 1295  rabid2 1309  reu2 1338  2reuswap 1341  isset 1351  ralv 1357  rexv 1358  ceqsrexv 1413  cbvab 1423  euxfr 1436  elrabsf 1456  nvelv 1483  dfss2 1497  dfss3 1498  dfss2f 1499  dfss3f 1500  sspsstri 1572  difdif 1595  unass 1615  unss 1632  inass 1650  symdif2 1690  unab 1691  inab 1692  n0f 1713  disj 1733  disj1 1734  disj2 1735  disj3 1736  undisj1 1739  undisj2 1740  ssdif0 1748  ssundif 1764  eltp 1834  snelpw 1861  sspwb 1863  pw0 1882  pwssun 1917  dfuni2 1921  unissb 1941  elint2 1972  ssint 1980  dfiun2 2014  dfiin2 2015  iunss 2017  ssiin 2024  iinss 2025  iunn0 2029  iundif2 2032  iindif2 2033  iunxun 2035  iinpw 2038  dftr2 2043  dftr5 2044  opabid 2099  dffr2 2171  ordtri4 2235  dflim2 2280  orddif 2326  onzsl 2367  opthprc 2457  elxp3 2460  elvv 2464  cbvop 2473  reluni 2493  cnvco 2520  cnvuni 2521  dmuni 2538  dmopab2 2541  dmxp 2552  elrn2 2563  dmres 2584  ssdmres 2585  dfima2 2604  dffr3 2620  cotr 2625  intasym 2627  intirr 2628  cnvopab 2632  cnv0 2633  cnvun 2642  cnvin 2643  rnuni 2646  cores 2659  coass 2667  dmco2 2673  dffun2 2674  dffunmof 2678  dffun6 2687  funfn 2689  fununi 2705  funin 2708  fnfrn 2758  fint 2769  fnforn 2791  funforn 2792  f1o4 2807  f1o5 2808  f1ocnv 2811  fsn 2895  f1fv 2916  iinon 2948  tfrlem5 2953  tfrlem7 2955  rdgsucopabn 2985  elrnoprab 3054  elxp6 3093  2o 3110  qsid 3237  domen 3284  brsdom 3286  brdom2 3292  mapsnen 3334  sbthlem10 3358  sbthcl 3361  brsdom2 3363  xpmapenlem5 3395  mapunen 3397  fiint 3445  trcl 3489  zfregs 3491  tz9.12lem3 3505  rankr1 3518  rankss 3531  cplem1 3545  aceq0 3553  aceq3lem 3555  aceq5lem2 3559  aceq5lem3 3560  aceq5 3563  aceq7 3566  kmlem3 3582  kmlem4 3583  kmlem11 3590  kmlem14 3593  kmlem15 3594  zorn2 3612  entri2 3646  unxpdomlem 3649  cardval2 3661  isinfcard 3692  iscard3 3693  elcard 3713  elni2 3799  distrpq 3861  psslinpr 3929  ltexprlem4 3939  ltresr 4052  ltmullem 4337  ltdivi 4398  creur 4532  creui 4533  elnnz 4572  elznn0nn 4575  elnn0nn 4593  nnwos 4610  uzwo3lem1 4614  seqlem2 4663  discrlem1 4713  nn0opthlem1 4722  sqr2irrlem4 4780  ruclem2 4886  ruclem8 4892  qnnen 4931  infxpidmlem2 4934  infxpidmlem7 4939  infxpidmlem8 4940  infmap2 4953  ocsh 5164  projlem4 5196  shne0 5372  spanun 5450  5oalem7 5550  pjnel 5665  cvbr2t 5715  cvnbtwn2t 5719  elat2 5739  chrelat2 5758

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