Theorem 3bitr4 183

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
3bitr4.1	|- (ph <-> ps)
3bitr4.2	|- (ch <-> ph)
3bitr4.3	|- (th <-> ps)

Assertion

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

Proof of Theorem 3bitr4

Step	Hyp	Ref	Expression
1		3bitr4.2	. 2 |- (ch <-> ph)
2		3bitr4.1	. . 3 |- (ph <-> ps)
3		3bitr4.3	. . 3 |- (th <-> ps)
4	2, 3	bitr4 176	. 2 |- (ph <-> th)
5	1, 4	bitr 173	1 |- (ch <-> th)

Syntax hints:   <-> wb 146

This theorem is referenced by:  orcom 246  orbi2i 255  or12 258  orass 260  or23 263  or4 264  pm4.78 354  pm4.79 355  anass 441  an23 487  an4 508  bicom 522  pm4.11 524  con2bi 527  oranabs 584  ordir 599  jcab 600  andi 606  andir 607  pm5.32ri 648  3anrot 782  3orrot 783  3ancoma 784  3anbi123i 824  3orbi123i 825  19.30 1087  19.32 1088  19.31 1089  19.43 1090  19.41 1097  19.42 1098  equsex 1154  cbvex 1168  dfsb3 1228  sbor 1237  sban 1239  sbbi 1241  sb8e 1264  sb6 1269  eeeanv 1326  sbel2x 1347  sbex 1350  sb8eu 1392  eu1 1394  cbvmo 1410  moanim 1429  euan 1430  eqcom 1480  abeq1 1572  clelab 1584  sbabel 1587  ralnex 1656  rexnal 1657  ralbii2 1674  rexbii2 1675  r2al 1679  r3al 1693  r2ex 1694  r19.26 1753  r19.32v 1761  r19.41v 1766  r19.42v 1767  r19.43 1768  ralcom 1777  rexcom 1778  reeanv 1781  reubiia 1784  cbvralf 1799  cbvrexf 1800  cbvrex 1802  cbvreuv 1805  eueq 1919  reu5 1932  reu2 1933  reu3 1934  reu6 1935  rmo4 1936  eqss 2081  dfpss3 2138  uncom 2180  unass 2191  ssequn1 2204  incom 2212  inass 2227  nssinpss 2244  nsspssun 2245  dfss4 2246  dfun2 2247  dfin2 2248  indi 2255  undi 2256  unab 2271  inab 2272  difab 2273  ne0f 2292  rabn0 2297  disj3 2319  ssdif0 2332  difin0ss 2337  inssdif0 2338  ssundif 2349  dfif2 2368  rexpr 2434  snprc 2448  r19.12sn 2449  eluni2 2512  elunirab 2519  uniun 2524  unissb 2533  elintrab 2550  intun 2567  intpr 2568  dfiun2g 2591  iunss 2596  ssiun 2597  ssiin 2604  iunin2 2614  iinun2 2615  iundif2 2616  iunxun 2620  iinuni 2621  iununi 2622  iinpw 2623  dftr2 2688  intexrab 2738  ssext 2770  pweqb 2772  opabid 2817  pwin 2832  pwun 2836  rexxfr 2908  dflim2 3032  unisuc 3053  sucexb 3055  sucelon 3075  onzsl 3124  dflim4 3126  opelxp 3221  rexxp 3226  brinxp2 3238  weinxp 3240  inopab 3275  inxp 3276  dmun 3324  dmuni 3326  dm0rn0 3337  brres 3380  asymref 3446  asymref2 3447  cnvun 3462  cnvin 3463  rnuni 3466  dminss 3469  imainss 3470  cnvxp 3471  rninxp 3489  resco 3507  rnco 3509  coass 3519  cnvpo 3529  cnvso 3530  funcnv 3564  funcnv3 3565  fncnv 3568  fun11 3569  funin 3573  imadif 3581  fint 3657  fin 3658  fores 3688  f1o2 3700  f1o3 3701  f1o4 3703  f1orn 3705  f11o 3719  imaiun 3871  isomin 3906  iinon 3917  dfrdg2 3940  dfoprab2 3998  dfopab2 4120  dfoprab3 4121  foprab2 4126  oarec 4203  erdmrn 4283  mapval2 4342  map0e 4349  elixp2 4356  elixp 4357  mapixp 4369  domen 4386  brsdom 4388  brdom2 4395  xpcomen 4446  xpassen 4448  pw2en 4453  brsdom2 4468  mapdom2 4501  xpmapenlem5 4507  fiint 4576  fiintOLD 4577  tz9.12lem3 4678  rankc1 4722  cp 4739  aceq1 4746  aceq2 4748  aceq3 4750  aceq5lem3 4754  ac6lem 4771  distrlem1pr 5146  ltexprlem1 5161  reclem2pr 5176  gt0srpr 5206  ltpsrpr 5238  subsub23 5393  negcon2 5427  leadd1 5611  lesubadd 5614  leneg 5623  lesub0 5631  ltreci 5887  sup3 6061  xrsupss 6087  elnn0z 6156  elnn0nn 6180  nnwof 6467  discrlem1 6664  nn0opthlem1 6672  sqrlem16 6696  crrecz 6749  cvganz 6931  infcvglem1 7228  infxpidmlem7 7566  infmap2lem1 7588  istps2 7615  isbasis2g 7618  tgval2t 7623  basgent 7646  ntreq0 7712  pilem1 8673  cosh111lem3 8718  efifolem2 8725  axgroth3 8781  grothprim 8785  h2hlm 8852  choc0 9292  chcon2 9389  chcon1 9390  chcon3 9391  chnle 9410  cmcm2 9538  cmcm3 9539  3oalem3 9611  pjdifnorm 9630  pjnel 9670  dfadj2 9814  cnvadj 9818  eleigvec2t 9884  nmop0 9912  nmfn0 9913  nmcopexlem1 9953  nmcfnexlem1 9982  rnbra 10042  pjima 10106  pjhmopidm 10112  cvnbtwn4t 10219  chrelat4 10303  ntunte 10442  cmpdom 10466

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