Theorem bitr4 176

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 172	. 2 |- (ps <-> ch)
4	1, 3	bitr 173	1 |- (ph <-> ch)

Syntax hints:   <-> wb 146

This theorem is referenced by:  3bitr2 179  3bitr2r 180  3bitr4 183  3bitr4r 184  imor 234  oridm 243  ianor 305  ioran 306  pm4.52 307  pm4.54 309  pm4.79 355  bi 513  bibi2i 606  pm5.32 642  pm5.6 686  mpbiran 726  mpbiran2 727  biluk 743  prlem2 769  3anrev 782  an6 899  19.33b 1088  19.41 1091  equsal 1147  sb5f 1198  sb3an 1233  sbequ8 1242  hbsb4t 1244  sb5 1263  sbel2x 1340  eu2 1389  eu3 1390  eu5 1402  moanim 1420  euan 1421  2eu4 1445  2eu6 1447  cleqf 1552  necon3bii 1590  neor 1630  neorian 1632  r2al 1668  r2ex 1683  r19.23v 1733  r19.26m 1744  r19.27av 1746  r19.29 1748  rabid2 1762  isset 1805  ralv 1811  rexv 1812  ceqsrexv 1880  cbvab 1899  reu2 1920  reu3 1921  reu6 1922  2reuswap 1927  elrabsf 1953  dfss2 2048  dfss3 2049  dfss2f 2050  dfss3f 2051  ssabral 2109  rabss 2114  sspsstri 2138  difdif 2156  unass 2177  unss 2194  inass 2213  unab 2257  inab 2258  ne0f 2277  eqv 2285  disj 2301  reldisj 2303  disj3 2304  undisj1 2310  undisj2 2311  ssdif0 2317  undif 2333  ralpr 2418  eltp 2429  pwpw0 2460  dfuni2 2495  unissb 2518  elint2 2530  ssint 2539  dfiin2 2578  iunss 2581  iinss 2590  iunn0 2597  iundif2 2600  iindif2 2601  iunxun 2604  iinpw 2607  dftr2 2672  dftr5 2673  dftr3 2674  nvelv 2703  notzfaus 2731  snelpw 2742  sspwb 2745  opabid 2799  pwssun 2816  dfid3 2826  dffr2 2909  ordtri4 2974  dflim2 3015  orddif 3065  onzsl 3107  opthprc 3211  elxp3 3214  elvv 3218  reluni 3255  cnvco 3289  cnvuni 3290  dmuni 3308  dmxp 3321  elrn 3336  dmres 3364  ssdmres 3365  dfima2 3389  args 3412  dffr3 3415  cotr 3420  intasym 3422  asymref 3423  asymrefOLD 3425  intirr 3427  cnvopab 3431  cnv0 3432  cnvun 3441  cnvin 3442  rnuni 3445  xpnz 3452  xp11 3463  cores 3485  resco 3486  imaco 3487  rnco 3488  coass 3498  cnvpo 3508  cnvso 3509  dffun2 3512  dffunmof 3516  dffun6 3525  funfn 3528  svrelfun 3546  fununi 3549  funin 3552  fnfrn 3619  fint 3635  fnforn 3662  f1o4 3681  f1o5 3682  f1ocnv 3686  fsn 3819  abexex 3858  f1fv 3859  tfrlem5 3900  tfrlem7 3902  dfrdg2 3918  rdgsucopabn 3932  elxp6 4086  elxp7 4087  fnoprab2g 4105  2on 4123  eqerlem 4254  qsid 4285  elixpconst 4335  domen 4361  brsdom 4363  brdom2 4369  sbthlem10 4436  sbthcl 4439  brsdom2 4441  xpmapenlem5 4480  mapunen 4482  trcl 4617  zfregs 4619  tz9.12lem3 4633  rankr1 4646  rankss 4660  cplem1 4692  aceq0 4702  aceq3lem 4704  aceq5lem2 4708  aceq5 4712  aceq7 4715  kmlem12 4748  kmlem14 4750  kmlem15 4751  zorn 4769  brdom7disj 4776  entri2 4812  unxpdomlem 4815  cardval2 4827  isinfcard 4859  iscard3 4860  elni2 4977  distrpq 5039  psslinpr 5107  ltexprlem4 5117  ltresr 5230  elxr 5508  prodge0 5776  ltdiv1i 5779  infm3 6001  xrinfmss 6026  dfn2 6059  elnnz 6092  elznn0nn 6095  elnn0nn 6118  seq1lem2 6247  elioo1t 6315  elioo2t 6316  elioc1t 6319  elico1t 6320  elicc1t 6321  snunioolem 6347  2rexuz 6378  nnwos 6392  elfz1t 6402  elfzuzb 6408  elfz2nn0t 6427  fznn0t 6448  discrlem1 6586  nn0opthlem1 6594  creur 6673  creui 6674  cvg3 6860  faclbnd4lem1 6885  climreu 7038  isumclimtf 7131  infcvglem1 7156  elcncf1d 7205  reefiso 7370  qnnen 7446  infxpidmlem2 7496  infxpidmlem7 7501  infxpidmlem8 7502  infmap2 7523  isbasis3g 7555  tgval2t 7559  fctop 7592  cctop 7594  ntreq0 7650  islp2 7688  blfval2 7776  metcnp4 7904  xpcn 7910  fsumcnlem 7923  bcthlem9 7941  bcthlem14 7946  nmobndseqi 8372  pilem3 8592  efif1lem5 8649  axgroth4 8719  grothprim 8722  hcau2 8976  ocsh 9072  projlem4 9105  spanun 9382  nonbool 9513  5oalem7 9522  adjsymt 9676  elbdop2t 9715  dmadjss 9736  eleigvect 9797  nmop0h 9831  nmcopexlem1 9866  nmcfnexlem1 9895  rnbra 9953  pjsspos 10011  pjord 10012  cvbr2t 10120  cvnbtwn2t 10124  mdsl2 10157  cvmd 10159  elat2 10175  atom1d 10188  chrelat2 10200  irred 10229  cdj3 10273  symgoprab 10307  ntunte 10340  abfi 10349  ficli 10368  hmeogrp 10425  cnfilca 10451

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