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  dfbi2 514  bibi2i 608  pm5.32 644  pm5.6 688  mpbiran 728  mpbiran2 729  biluk 745  prlem2 771  3anrev 784  an6 902  19.33b 1092  19.41 1095  equsal 1151  sb5f 1202  sb3an 1238  sbequ8 1247  hbsb4t 1249  sb5 1268  sbel2x 1345  eu2 1396  eu3 1397  eu5 1409  moanim 1427  euan 1428  2eu4 1452  2eu6 1454  cleqf 1559  necon3bii 1597  neor 1637  neorian 1639  r2al 1675  r2ex 1690  r19.23v 1740  r19.26m 1751  r19.27av 1753  r19.29 1755  rabid2 1769  isset 1812  ralv 1818  rexv 1819  ceqsrexv 1887  cbvab 1906  reu2 1928  reu3 1929  reu6 1930  2reuswap 1935  elrabsf 1961  dfss2 2056  dfss3 2057  dfss2f 2058  dfss3f 2059  ssabral 2117  rabss 2122  sspsstri 2146  difdif 2164  unass 2185  unss 2202  inass 2221  unab 2265  inab 2266  ne0f 2285  eqv 2293  disj 2309  reldisj 2311  disj3 2312  undisj1 2318  undisj2 2319  ssdif0 2325  undif 2341  ralpr 2426  eltp 2437  pwpw0 2467  dfuni2 2503  unissb 2526  elint2 2538  ssint 2547  dfiin2 2586  iunss 2589  iinss 2598  iunn0 2605  iundif2 2608  iindif2 2609  iunxun 2612  iinpw 2615  dftr2 2680  dftr5 2681  dftr3 2682  nvelv 2711  notzfaus 2739  snelpw 2750  sspwb 2753  opabid 2808  pwssun 2825  dfid3 2834  dffr2 2917  ordtri4 2982  dflim2 3023  orddif 3073  onzsl 3115  opthprc 3219  elxp3 3222  elvv 3226  reluni 3263  cnvco 3298  cnvuni 3299  dmuni 3317  dmxp 3330  elrn 3348  dmres 3378  ssdmres 3379  dfima2 3403  args 3426  dffr3 3429  cotr 3434  intasym 3436  asymref 3437  intirr 3439  cnvopab 3443  cnv0 3444  cnvun 3453  cnvin 3454  rnuni 3457  xpnz 3464  xp11 3474  cores 3497  resco 3498  imaco 3499  rnco 3500  coass 3510  cnvpo 3520  cnvso 3521  dffun2 3524  dffunmof 3528  dffun6 3537  funfn 3540  svrelfun 3558  fununi 3561  funin 3564  fnfrn 3632  fint 3648  fnforn 3675  f1o4 3694  f1o5 3695  f1ocnv 3699  fsn 3832  abexex 3871  f1fv 3872  tfrlem5 3913  tfrlem7 3915  dfrdg2 3931  rdgsucopabn 3945  elxp6 4100  elxp7 4101  fnoprab2g 4119  2on 4137  eqerlem 4268  qsid 4299  elixpconst 4349  domen 4375  brsdom 4377  brdom2 4383  sbthlem10 4450  sbthcl 4453  brsdom2 4455  xpmapenlem5 4494  mapunen 4496  trcl 4633  zfregs 4635  tz9.12lem3 4649  rankr1 4662  rankss 4676  cplem1 4708  aceq0 4718  aceq3lem 4720  aceq5lem2 4724  aceq5 4728  aceq7 4731  kmlem12 4764  kmlem14 4766  kmlem15 4767  zorn 4785  brdom7disj 4792  entri2 4828  unxpdomlem 4831  cardval2 4843  isinfcard 4875  iscard3 4876  elni2 4993  distrpq 5055  psslinpr 5123  ltexprlem4 5133  ltresr 5246  elxr 5523  prodge0 5791  ltdiv1i 5794  infm3 6022  xrinfmss 6047  dfn2 6080  elnnz 6113  elznn0nn 6116  elnn0nn 6139  seq1lem2 6274  elioo1t 6342  elioo2t 6343  elioc1t 6346  elico1t 6347  elicc1t 6348  snunioolem 6374  2rexuz 6406  nnwos 6420  elfz1t 6430  elfzuzb 6436  elfz2nn0t 6455  fznn0t 6476  discrlem1 6616  nn0opthlem1 6624  creur 6702  creui 6703  cvg3 6881  faclbnd4lem1 6906  climreu 7059  isumclimtf 7153  infcvglem1 7179  elcncf1d 7228  reefiso 7385  qnnen 7460  infxpidmlem2 7510  infxpidmlem7 7515  infxpidmlem8 7516  infmap2 7538  isbasis3g 7570  tgval2t 7574  fctop 7607  cctop 7609  ntreq0 7665  islp2 7704  blfval2 7793  metcnp4 7927  xpcn 7933  fsumcnlem 7946  bcthlem9 7964  bcthlem14 7969  nmobndseqi 8397  pilem3 8630  efif1lem5 8689  axgroth4 8735  grothprim 8738  hcau2 9010  ocsh 9111  projlem4 9144  spanun 9422  nonbool 9551  5oalem7 9560  adjsymt 9714  elbdop2t 9753  dmadjss 9774  eleigvect 9836  nmop0h 9871  nmcopexlem1 9906  nmcfnexlem1 9935  rnbra 9995  pjsspos 10055  pjord 10056  cvbr2t 10165  cvnbtwn2t 10169  mdsl2 10204  cvmd 10206  elat2 10222  atom1d 10235  chrelat2 10247  irred 10276  cdj3 10323  symgoprab 10357  ntunte 10394  abfi 10403  ficli 10422  hmeogrp 10480  cnfilca 10506

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