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 608  bibi1i 609  pm5.32 644  pm5.55 675  rnlem 773  an6 902  19.43 1088  alrot4 1097  excom13 1098  sb3an 1238  19.12vv 1302  3exdistr 1312  4exdistr 1313  ee4anv 1325  2exsb 1351  2eu4 1452  2eu6 1454  2eu7 1455  2eu8 1456  r19.29 1756  ceqsex2 1836  gencbvex 1838  reu2 1930  reu3 1931  rmo4 1933  reu8 1936  sbralie 1941  elrabsf 1963  dfss2 2058  ss2rab 2123  rabss 2124  ssrab 2125  symdif2 2266  reuun2 2278  dfnul2 2282  abn0 2290  disj 2311  disj4 2317  inssdif0 2333  elimif 2374  ralpr 2428  eltp 2439  r19.12sn 2444  difprsn 2465  prsspw 2480  preqsn 2486  uni0b 2523  uni0c 2524  unissb 2528  ssint 2549  ssintab 2550  iunconst 2572  dfiin2 2588  iunss 2591  iunrab 2596  ssiin 2599  iunid 2603  iunn0 2607  iunxsn 2612  iunxun 2614  dftr5 2683  ssextss 2762  exss 2769  eqvinop 2791  opeqsn 2802  opeqpr 2803  brabsb 2816  opabn0 2824  dfid3 2836  uniuni 2880  euuni 2881  reusn 2892  dfwe2 2935  wereu 2945  ordtri3or 2979  ordtri1 2980  ordtri3 2983  ordpwsuc 3066  onzsl 3117  dfom2 3133  relop 3275  cnvco 3300  cnvuni 3301  dmuni 3319  dmopab3 3322  dmcosseq 3365  opelres 3372  dfima2 3405  elimasn 3426  asymref 3439  asymref2 3440  intirr 3441  cnvsn 3449  elxp4 3453  elxp5 3454  rnuni 3459  xpeq0 3467  ssrnres 3481  dminxp 3483  imaco 3501  rnco 3502  coi1 3510  cnvpo 3522  dffun2 3526  fncnv 3561  fun11 3562  isarep1 3577  fcoi1 3645  fcoi2 3646  f1cnv 3666  f1o5 3697  fv2 3720  fnressn 3837  imaiun 3864  f1fv 3874  f1ofv 3877  dfrdg2 3933  tz7.48lem 3955  tz7.49c 3960  1st2val 4095  2nd2val 4096  foprab2 4119  elrnoprabg 4124  oaord 4181  eqerlem 4270  th3qlem1 4314  mapsnen 4429  xpsnen 4435  xpassen 4441  pw2en 4446  dom0 4465  abfii2OLD 4562  tz9.12lem3 4661  ranksn 4689  rankeq0 4696  rankxpsuc 4715  cp 4722  aceq5lem1 4735  aceq5lem2 4736  aceq5lem5 4739  kmlem3 4767  kmlem12 4776  kmlem13 4777  kmlem14 4778  kmlem15 4779  aceqkm 4781  cf0 4910  ltpiord 5015  genpn0 5106  genpass 5112  distrlem1pr 5127  psslinpr 5135  suplem1pr 5161  suplem2pr 5162  mappsrpr 5218  opelreal 5249  elreal 5250  neg11 5406  ltxrt 5495  elxr 5535  ssxr 5540  lesubadd 5595  divmul13t 5782  halfpos 5904  xrsupss 6078  xrinfmss 6079  elnn0 6101  elnn0z 6147  elznn0nn 6148  raluz2 6443  rexuz2 6445  nnwos 6460  elfzuzb 6476  sqeqor 6647  cjreb 6781  negreb 6795  abs00 6842  cau3ir 6915  cau5 6919  bcpasc 6969  expcnvlem2 7228  infpn2 7509  ruclem1 7510  ruclem3 7512  infxpidmlem8 7559  infxpidmlem9 7560  istps3 7608  tgval2t 7617  subbasOLD 7644  subtop 7646  cctop 7652  qdensere 7751  spwpr2 8658  pilem1 8671  hlimcaui 9106  choc0 9290  shlesb1 9359  shne0 9371  chnle 9408  h1deot 9472  cmbr2 9539  pjss2 9625  pjnel 9668  ho02 9755  adjsymt 9759  lnopeq 9933  dfpjopt 10111  large 10194  atoml2 10310  cdj3lem3b 10367  eeeeanv 10436  ntunte 10439  hmeogrp 10538

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