Theorem 3bitr4i 200

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence.

Hypotheses

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

Assertion

Ref	Expression
3bitr4i	|- (ch <-> th)

Proof of Theorem 3bitr4i

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

Syntax hints:   <-> wb 163

This theorem is referenced by:  orcom 266  orbi2i 275  or12 278  orassOLD 281  or23OLD 285  or4 286  pm4.78 381  pm4.79 382  anass 487  an23 543  an4 564  bicom 579  notbi 581  con2bi 584  oranabs 642  ordir 658  jcab 659  andi 665  andir 666  bibi2i 669  pm5.32ri 708  pm5.18 722  3anrot 863  3orrot 864  3ancoma 865  3orcomb 867  3anor 869  3anbi123i 1056  3orbi123i 1057  nic-justlem 1231  nic-axALT 1240  19.26-3an 1418  19.30OLD 1437  19.32 1438  19.31 1439  19.43 1440  19.41OLD 1449  19.42 1450  equsex 1513  cbvex 1529  dfsb3 1596  sbor 1605  sban 1607  sbbi 1609  sb8e 1639  sb6 1644  eeeanv 1708  eeeanvOLD 1709  sbel2x 1736  sbex 1739  sb8eu 1783  sb8euOLD 1784  eu1 1786  sbmo 1796  cbvmo 1804  moanim 1826  euanOLD 1828  eqcom 1886  abeq1 2000  clelab 2013  sbabel 2016  ralnex 2113  rexnal 2114  ralbii2 2131  rexbii2 2132  r2al 2136  r3al 2151  r2ex 2152  r19.23 2206  r19.26OLD 2220  r19.32v 2230  r19.41 2235  r19.42v 2237  r19.43 2238  r19.43OLD 2239  ralcom 2242  rexcom 2243  reean 2247  reeanOLD 2248  rabid2 2254  reubiia 2261  cbvralf 2276  cbvrexf 2277  cbvreuv 2282  vjust 2293  ceqsex3v 2330  ceqsex4v 2331  ceqsex8v 2333  ralrab 2418  cbvab 2419  eueq 2427  reu5 2441  reu2 2442  reu6 2443  reu3 2444  rmo4 2445  eqss 2631  dfpss3OLD 2696  uncomOLD 2745  unassOLD 2760  ssequn1 2775  ssequn1OLD 2776  ralunb 2784  incom 2787  inass 2804  ssin 2814  nssinpss 2824  nssinpssOLD 2825  nsspssun 2826  dfss4OLD 2828  dfun2 2829  dfin2 2830  difin 2831  indi 2838  indiOLD 2839  undiOLD 2841  symdif2 2857  unabOLD 2860  inabOLD 2862  difabOLD 2864  ne0f 2883  rabn0 2893  disj3 2918  ssdif0 2934  difin0ss 2939  inssdif0 2940  inssdif0OLD 2941  ssundif 2955  dfif2 2984  pwjustOLD 3034  ralprOLD 3080  rexpr 3082  raltp 3083  disjsn 3089  snprc 3092  r19.12sn 3093  prss 3138  tpss 3145  eluni2 3181  elunirab 3190  uniun 3196  unissb 3208  elintrab 3228  intun 3249  intpr 3250  iuncom 3261  dfiun2gOLD 3284  dfiin2 3287  cbviun 3289  iunssOLD 3292  ssiunOLD 3294  ssiinOLD 3303  iunn0 3315  iunin2 3320  iinun2 3321  iundif2 3322  iunxun 3329  iinuni 3330  iununi 3331  iununiOLD 3332  sspwuni 3333  iinpw 3336  brab1 3384  brun 3387  brin 3388  brdif 3389  dftr2 3413  intexrab 3468  inuni 3470  ssext 3508  pweqb 3511  opabidOLD 3558  opelopabsb 3564  pwin 3576  pwun 3580  dflim2 3719  unisuc 3741  euexeqOLD 3826  euexaleq 3827  rexxfr 3841  sucexb 3890  sucelon 3898  onzslOLD 3929  dflim4 3932  opelxpOLD 4037  rexxp 4042  rexxpf 4044  iunxpf 4045  brinxp2 4057  weinxp 4059  inopab 4108  inxpOLD 4110  cnvco 4145  dmunOLD 4164  dmuni 4166  dm0rn0 4175  brres 4223  cnvsym 4304  asymref 4308  asymrefOLD 4309  asymref2OLD 4311  intirr 4312  cnvopab 4317  cnvunOLD 4323  cnvin 4324  rnuni 4327  dminss 4330  imainss 4331  cnvxpOLD 4333  rninxpOLD 4356  dmsnn0 4362  dmsnop 4367  coundiOLD 4397  coundirOLD 4399  resco 4402  rnco 4404  coiun 4407  coass 4415  cnvpo 4427  cnvso 4428  funcnv 4475  funcnv3 4476  fncnv 4479  fun11 4480  funinOLD 4485  imadif 4493  iunfopabOLD 4543  fint 4591  fintOLD 4592  fin 4593  finOLD 4594  fores 4627  dff1o2 4639  dff1o2OLD 4640  dff1o3 4641  dff1o3OLD 4642  dff1o4OLD 4645  f1orn 4648  f11o 4666  imaiun 4840  isomin 4876  dfoprab2 4917  dfopab2 5053  dfoprab3 5054  foprab2 5061  fsplit 5086  iinon 5115  onopriun 5118  dfrdg2 5141  oarec 5244  erdmrn 5334  uniqs 5354  mapval2 5394  map0e 5401  elixp2 5408  elixp 5409  mapixp 5421  domen 5438  brsdom 5440  brdom2 5447  xpcomen 5498  xpassen 5500  pw2en 5505  brsdom2 5524  mapdom2 5588  xpmapenlem5 5594  fiint 5650  tz9.12lem3 5772  rankc1 5816  cp 5852  aceq1 5891  aceq2 5893  aceq3 5895  aceq5lem3 5899  ac6lem 5916  distrlem1pr 6279  ltexprlem1 6294  reclem2pr 6309  gt0srpr 6339  ltpsrpr 6371  subsub23i 6531  negcon2i 6568  leadd1i 6767  lesubaddiOLD 6772  lenegi 6784  lesub0i 6792  lesub0iOLD 6793  ltrecii 7061  sup3 7261  xrsupss 7287  elnn0z 7356  elnn0nn 7380  nnwof 7628  discrlem1 7906  nn0opthlem1 7914  sqrlem16 7938  crreczi 7991  cvganz 8176  infcvglem1 8482  infxpidmlem7 8827  infmap2lem1 8848  istps2 8876  isbasis2g 8881  tgval2 8887  basgen 8910  ntreq0 8984  pilem1 10020  cosh111lem3 10070  efifolem2 10077  axgroth6 10137  axgroth3 10138  grothprim 10141  oprabopabf 10157  isfbas2 10263  elfg 10284  filrn 10293  h2hlm 10482  choc0 10923  chcon2i 11020  chcon1i 11021  chcon3i 11022  chnlei 11041  cmcm2i 11169  cmcm3i 11170  3oalem3 11244  pjdifnormii 11263  pjneli 11303  dfadj2 11449  cnvadj 11453  eleigvec2 11519  nmop0 11547  nmfn0 11548  nmcopexlem1 11588  nmcfnexlem1 11617  rnbra 11678  pjimai 11748  pjhmopidm 11754  cvnbtwn4 11861  chrelat4i 11945  bnj172OLD 12039  bnj193OLD 12064  bnj257 12096  bnj268 12107  bnj279OLD 12119  bnj290 12130  bnj301OLD 12142  bnj312 12153  bnj334OLD 12176  bnj345OLD 12188  bnj378OLD 12223  bnj389OLD 12235  bnj400OLD 12247  bnj411OLD 12259  bnj422OLD 12271  bnj434OLD 12283  bnj445OLD 12295  bnj456OLD 12307  bnj467OLD 12319  bnj479OLD 12331  bnj490OLD 12343  bnj500OLD 12355  bnj11OLD 12377  bnj24 12388  bnj25OLD 12393  bnj39OLD 12411  bnj47OLD 12418  bnj54 12428  bnj55 12430  bnj58 12431  bnj62OLD 12434  bnj77 12437  bnj77OLD 12438  bnj78 12439  bnj89 12444  bnj574 12546  bnj575 12547  bnj576 12548  bnj887 12810  bnj912 12822  bnj913 12823  bnj971 12860  bnj1019 12878  bnj1088 12910  bnj1146 12943  bnj1185 12967  bnj1289 13037  bnj1306 13049  bnj1310 13050  bnj1385 13102  bnj1394 13108  bnj1402 13112  bnj1492 13161  bnj70 13205  bnj119 13229  bnj121 13231  bnj130 13240  bnj153 13247  bnj543 13269  bnj607 13304  bnj849 13318  bnj882 13320  bnj985 13359  bnj1040 13388  bnj1067 13399  bnj1083 13408  bnj1128 13428  bnj1137 13433  divalglem4 13699  divalglem10 13705  1nprm 13769  zgt1b2 13772  isprm2lem 13774  isprm2 13775  isprm3 13776  untuni 13797  3or6 13804  3ioran 13808  r19.30 13817  ralunbOLD 13819  indifdi 13823  dif2relOLD 13828  dffr5 13831  dftr6 13834  wfrlem11 13967  tfrALTlem 13976  elsymdif 14062  symdif2rel 14064  brsset 14069  idsset 14070  dfon3 14072  brbigcup 14074  ellimits 14079  df3nandALT1 14146  imnand2 14149  assxor 14279  fates 14292  bidia 14315  evevifev 14328  restidsing 14391  omslim 14420  omslim2 14421  cmpdom 14481  trooo 14758  cinvlem3 15178  bpmp 15251  cnvresima 15359  trer 15361  opncldf1 15402  compfipin0 15436  alexsublem2 15438  alexsublem4 15440  is1stc3 15469  isfne2 15481  locfincomp 15514  filssufillem 15570  sbmoOLD 15654  3reeanv 15661  ralrabOLD 15670  prfOLD 15680  opabex3 15701  inixp 15722  sstotbnd 15936  isidl 16162  isfldidl2 16217  isdmn3 16222  pm10.541 16314  pm11.07 16321  elnev 16404  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  conss34 16419  conss1 16421  elstrscaf 16716  stb2xpl 16742  stb3xpl 16743  pmapglbx 17251

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 164

Copyright terms: Public domain