Theorem 3bitr 177

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 173	. 2 |- (ps <-> th)
5	1, 4	bitr 173	1 |- (ph <-> th)

Syntax hints:   <-> wb 146

This theorem is referenced by:  orbi1i 256  pm4.14 352  pm4.15 353  anbi1i 481  bibi2i 607  bibi1i 608  pm5.32 643  pm5.55 674  rnlem 772  an6 900  19.43 1086  alrot4 1095  excom13 1096  sb3an 1236  19.12vv 1300  3exdistr 1310  4exdistr 1311  ee4anv 1323  2exsb 1349  2eu4 1450  2eu6 1452  2eu7 1453  2eu8 1454  r19.29 1753  ceqsex2 1832  gencbvex 1834  reu2 1926  reu3 1927  rmo4 1929  reu8 1932  sbralie 1937  elrabsf 1959  dfss2 2054  ss2rab 2119  rabss 2120  ssrab 2121  symdif2 2262  reuun2 2274  dfnul2 2278  abn0 2286  disj 2307  disj4 2313  inssdif0 2329  elimif 2370  ralpr 2424  eltp 2435  r19.12sn 2440  difprsn 2461  prsspw 2476  preqsn 2482  uni0b 2518  uni0c 2519  unissb 2523  ssint 2544  ssintab 2545  iunconst 2567  dfiin2 2583  iunss 2586  iunrab 2591  ssiin 2594  iunid 2598  iunn0 2602  iunxsn 2607  iunxun 2609  dftr5 2678  ssextss 2757  exss 2764  eqvinop 2786  opeqsn 2797  opeqpr 2798  brabsb 2811  opabn0 2819  dfid3 2831  uniuni 2875  euuni 2876  reusn 2887  dfwe2 2930  wereu 2940  ordtri3or 2974  ordtri1 2975  ordtri3 2978  ordpwsuc 3061  onzsl 3112  dfom2 3128  relop 3270  cnvco 3295  cnvuni 3296  dmuni 3314  dmopab3 3317  dmcosseq 3357  opelres 3364  dfima2 3397  elimasn 3418  asymref 3431  asymref2 3432  intirr 3433  cnvsn 3441  elxp4 3445  elxp5 3446  rnuni 3451  xpeq0 3459  ssrnres 3473  dminxp 3475  imaco 3493  rnco 3494  coi1 3502  cnvpo 3514  dffun2 3518  fncnv 3553  fun11 3554  isarep1 3569  fcoi1 3636  fcoi2 3637  f1cnv 3657  f1o5 3688  fv2 3711  fnressn 3828  imaiun 3855  f1fv 3865  f1ofv 3868  dfrdg2 3924  tz7.48lem 3946  tz7.49c 3951  1st2val 4085  2nd2val 4086  foprab2 4109  elrnoprabg 4114  oaord 4171  eqerlem 4260  th3qlem1 4304  mapsnen 4416  xpsnen 4421  xpassen 4427  pw2en 4432  dom0 4451  abfii2 4542  tz9.12lem3 4641  ranksn 4669  rankeq0 4676  rankxpsuc 4695  cp 4702  aceq5lem1 4715  aceq5lem2 4716  aceq5lem5 4719  kmlem3 4747  kmlem12 4756  kmlem13 4757  kmlem14 4758  kmlem15 4759  aceqkm 4761  cf0 4890  ltpiord 4995  genpn0 5086  genpass 5092  distrlem1pr 5107  psslinpr 5115  suplem1pr 5141  suplem2pr 5142  mappsrpr 5198  opelreal 5229  elreal 5230  neg11 5386  ltxrt 5475  elxr 5516  ssxr 5521  lesubadd 5577  divmul13t 5746  halfpos 5860  xrsupss 6033  xrinfmss 6034  elnn0 6056  elnn0z 6102  elznn0nn 6103  raluz2 6383  rexuz2 6385  nnwos 6400  elfzuzb 6416  sqeqor 6586  cjreb 6724  negreb 6738  abs00 6785  absgt0 6786  cau3ir 6860  cau5 6864  bcpasc 6915  expcnvlem2 7171  infpn2 7460  ruclem1 7461  ruclem3 7463  infxpidmlem8 7510  infxpidmlem9 7511  istps3 7558  tgval2t 7567  subbas 7594  subtop 7596  cctop 7602  qdensere 7701  pilem1 8609  hlimcaui 9045  choc0 9228  shlesb1 9297  shne0 9309  chnle 9346  h1deot 9410  cmbr2 9479  pjss2 9565  pjnel 9608  ho02 9695  adjsymt 9699  lnopeq 9871  dfpjopt 10049  large 10132  atoml2 10247  cdj3lem3b 10301  eeeeanv 10372  ntunte 10376  hmeogrp 10461

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