Theorem 3bitri 175

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitri

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

Syntax hints:   <-> wb 144

This theorem is referenced by:  orbi1i 254  pm4.14 350  pm4.15 351  anbi1i 484  bibi2i 611  bibi1i 612  pm5.32 647  pm5.55 679  rnlem 778  an6 908  nic-axALT 970  19.43 1124  alrot4 1133  excom13 1134  sb3an 1275  19.12vv 1340  3exdistr 1350  4exdistr 1351  ee4anv 1363  2exsb 1390  2eu4 1492  2eu6 1494  2eu7 1495  2eu8 1496  r19.29 1802  ceqsex2 1882  gencbvex 1884  reu2 1976  reu3 1977  rmo4 1979  reu8 1982  sbralie 1986  elrabsf 2011  dfss2 2110  ss2rab 2175  rabss 2176  ssrab 2177  symdif2 2318  reuun2 2330  dfnul2 2334  abn0 2343  disj 2364  disj4 2370  inssdif0 2386  elimif 2428  ralpr 2486  ralsn 2488  eltp 2500  r19.12sn 2505  difprsn 2529  prsspw 2545  preqsn 2551  uni0b 2590  uni0c 2591  unissb 2595  ssint 2616  ssintab 2617  iunconst 2640  dfiin2 2656  iunss 2659  iunrab 2664  ssiin 2667  iunn0 2676  iunxsn 2682  iunxun 2684  dftr5 2757  axpweq 2817  ssextss 2839  exss 2847  eqvinop 2867  opeqsn 2879  opeqpr 2880  brabsb 2893  opabn0 2902  dfid3 2914  posn 2928  wereu 2972  ordtri3or 3007  ordtri1 3008  ordtri3 3011  uniuni 3104  euuni 3105  reusn 3115  dfwe2 3140  ordpwsuc 3172  onzsl 3200  dfom2 3220  elvvv 3314  reliun 3354  relop 3365  cnvco 3391  cnvuni 3392  dmuni 3410  dmopab3 3413  dmcosseq 3452  opelres 3459  dfima2 3497  elimasn 3518  asymref 3531  asymref2 3532  intirr 3533  rnuni 3544  xpeq0 3552  ssrnres 3566  dminxp 3568  cnvsn 3580  elxp4 3585  elxp5 3586  dfco2a 3599  imaco 3604  rnco 3605  coi1 3614  cnvpo 3627  dffun2 3631  fncnv 3666  fun11 3667  isarep1 3683  fcoi1 3752  fcoi2 3753  f1cnv 3773  dff1o5 3805  fv2 3831  fnressn 3951  imaiun 3978  dff13 3988  dff1o6 3991  foprab2 4181  elrnoprabg 4186  fparlem1 4199  fparlem2 4200  fparlem3 4201  fparlem4 4202  dfrdg2 4234  tz7.48lem 4256  tz7.49c 4261  oaord 4317  eqerlem 4410  uniqs 4436  th3qlem1 4455  mapsnen 4570  xpsnen 4576  xpassen 4582  pw2en 4587  dom0 4610  abfii2 4705  tz9.12lem3 4807  ranksn 4835  rankeq0 4842  rankxpsuc 4861  cp 4868  aceq5lem1 4881  aceq5lem2 4882  aceq5lem5 4885  kmlem3 4913  kmlem12 4922  kmlem13 4923  kmlem14 4924  kmlem15 4925  aceqkm 4927  cf0 5060  ltpiord 5169  genpn0 5260  genpass 5266  distrlem1pr 5281  psslinpr 5289  suplem1pr 5315  suplem2pr 5316  mappsrpr 5372  opelreal 5403  elreal 5404  neg11i 5560  ltxr 5649  elxr 5689  ssxr 5694  lesubaddi 5749  halfposi 6049  xrsupss 6246  xrinfmss 6247  elnn0 6269  elnn0z 6315  elznn0nn 6316  raluz2 6570  rexuz2 6572  nnwos 6587  elfzuzb 6604  sqeqori 6844  cjrebi 6982  negrebi 6996  abs00i 7044  cau3iri 7118  cau5i 7122  bcpasci 7172  expcnvlem2 7432  infpn2 7721  ruclem1 7722  ruclem3 7724  infxpidmlem8 7771  infxpidmlem9 7772  istps3 7820  tgval2 7829  subbas 7856  subtop 7858  cctop 7862  qdensere 7961  spwpr2 8920  pilem1 8938  grothpw 9054  hlimcauii 9382  choc0 9566  shlesb1i 9635  shne0i 9647  chnlei 9684  h1deoi 9748  cmbr2i 9815  pjss2i 9903  pjneli 9946  ho02i 10035  adjsym 10039  lnopeqi 10212  dfpjop 10391  largei 10475  atoml2i 10592  cdj3lem3b 10649  anddi2 10718  eeeeanv 10720  ntunte 10728  ref3w 10772  definc 10869  hmeogrp 11044  sbtpsines 11062  cnvresima 11407  ordiso 11426  subntr 11482  compsub 11488  compfipin0 11493  alexsublem3 11498  alexsublem4 11499  reconnlem1 11507  filrn 11643  cnfillim 11687  difin2 11791  difxp 11798  opabex3 11806  eqfnfv3 11819  fimaxre 11856  isbnd3 11997  heiborlem24 12034  heiborlem29 12039

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 145

Copyright terms: Public domain