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 480  bibi2i 606  bibi1i 607  pm5.32 642  pm5.55 673  rnlem 771  an6 899  19.43 1084  alrot4 1093  excom13 1094  sb3an 1233  19.12vv 1297  3exdistr 1307  4exdistr 1308  ee4anv 1320  2exsb 1346  2eu4 1445  2eu6 1447  2eu7 1448  2eu8 1449  r19.29 1748  ceqsex2 1827  gencbvex 1829  reu2 1920  reu3 1921  rmo4 1923  reu8 1926  sbralie 1931  elrabsf 1953  dfss2 2048  ss2rab 2113  rabss 2114  ssrab 2115  symdif2 2256  reuun2 2268  dfnul2 2272  abn0 2280  disj 2301  disj4 2307  inssdif0 2323  elimif 2364  ralpr 2418  eltp 2429  r19.12sn 2434  difprsn 2456  prsspw 2471  preqsn 2477  uni0b 2513  uni0c 2514  unissb 2518  ssint 2539  ssintab 2540  iunconst 2562  dfiin2 2578  iunss 2581  iunrab 2586  ssiin 2589  iunid 2593  iunn0 2597  iunxsn 2602  iunxun 2604  dftr5 2673  ssextss 2752  exss 2759  eqvinop 2781  opeqsn 2791  opeqpr 2792  brabsb 2805  opabn0 2813  dfid3 2826  uniuni 2870  euuni 2871  reusn 2882  dfwe2 2925  wereu 2935  ordtri1 2970  ordtri3 2973  ordpwsuc 3056  onzsl 3107  dfom2 3123  relop 3265  cnvco 3289  cnvuni 3290  dmuni 3308  dmopab3 3311  dmcosseq 3349  opelres 3356  dfima2 3389  elimasn 3410  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  intirr 3427  cnvsn 3435  elxp4 3439  elxp5 3440  rnuni 3445  xpeq0 3453  ssrnres 3467  dminxp 3469  imaco 3487  rnco 3488  coi1 3496  cnvpo 3508  dffun2 3512  fncnv 3547  fun11 3548  isarep1 3563  fcoi1 3630  fcoi2 3631  f1cnv 3651  f1o5 3682  fv2 3705  fnressn 3822  imaiun 3849  f1fv 3859  f1ofv 3862  dfrdg2 3918  tz7.48lem 3940  tz7.49c 3945  1st2val 4079  2nd2val 4080  foprab2 4103  elrnoprabg 4108  oaord 4165  eqerlem 4254  th3qlem1 4298  mapsnen 4410  xpsnen 4415  xpassen 4421  pw2en 4426  dom0 4445  abfii2 4536  tz9.12lem3 4633  ranksn 4661  rankeq0 4668  rankxpsuc 4687  cp 4694  aceq5lem1 4707  aceq5lem2 4708  aceq5lem5 4711  kmlem3 4739  kmlem12 4748  kmlem13 4749  kmlem14 4750  kmlem15 4751  aceqkm 4753  cf0 4882  ltpiord 4987  genpn0 5078  genpass 5084  distrlem1pr 5099  psslinpr 5107  suplem1pr 5133  suplem2pr 5134  mappsrpr 5190  opelreal 5221  elreal 5222  neg11 5378  ltxrt 5467  elxr 5508  ssxr 5513  lesubadd 5569  divmul13t 5738  halfpos 5852  xrsupss 6025  xrinfmss 6026  elnn0 6048  elnn0z 6094  elznn0nn 6095  raluz2 6375  rexuz2 6377  nnwos 6392  elfzuzb 6408  sqeqor 6578  cjreb 6716  negreb 6730  abs00 6777  absgt0 6778  cau3ir 6852  cau5 6856  bcpasc 6907  expcnvlem2 7163  infpn2 7452  ruclem1 7453  ruclem3 7455  infxpidmlem8 7502  infxpidmlem9 7503  istps3 7550  tgval2t 7559  subbas 7586  subtop 7588  cctop 7594  qdensere 7691  pilem1 8590  hlimcaui 9027  choc0 9205  shlesb1 9274  shne0 9286  chnle 9323  h1deot 9387  cmbr2 9456  pjss2 9542  pjnel 9585  ho02 9672  adjsymt 9676  lnopeq 9848  dfpjopt 10021  large 10104  atoml2 10218  cdj3lem3b 10272  eeeeanv 10336  ntunte 10340  hmeogrp 10425

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