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 439  an23 484  an4 505  bicom 518  pm4.11 520  con2bi 523  oranabs 580  ordir 595  jcab 596  andi 602  andir 603  pm5.32ri 644  3anrot 778  3orrot 779  3ancoma 780  3anbi123i 820  3orbi123i 821  19.30 1081  19.32 1082  19.31 1083  19.43 1084  19.41 1091  19.42 1092  equsex 1148  cbvex 1162  dfsb3 1221  sbor 1230  sban 1232  sbbi 1234  sb8e 1257  sb6 1262  eeeanv 1319  sbel2x 1340  sbex 1343  sb8eu 1383  eu1 1385  cbvmo 1401  moanim 1420  euan 1421  eqcom 1469  abeq1 1561  clelab 1573  sbabel 1576  ralnex 1645  rexnal 1646  ralbii2 1663  rexbii2 1664  r2al 1668  r3al 1682  r2ex 1683  r19.26 1742  r19.32v 1750  r19.41v 1755  r19.42v 1756  r19.43 1757  ralcom 1766  rexcom 1767  reeanv 1770  reubiia 1773  cbvralf 1788  cbvrex 1790  cbvreuv 1793  eueq 1907  reu5 1919  reu2 1920  reu3 1921  reu6 1922  rmo4 1923  eqss 2067  dfpss3 2124  uncom 2166  unass 2177  ssequn1 2190  incom 2198  inass 2213  nssinpss 2230  nsspssun 2231  dfss4 2232  dfun2 2233  dfin2 2234  indi 2241  undi 2242  unab 2257  inab 2258  difab 2259  ne0f 2277  rabn0 2282  disj3 2304  ssdif0 2317  difin0ss 2322  inssdif0 2323  ssundif 2334  dfif2 2353  rexpr 2419  snprc 2433  r19.12sn 2434  eluni2 2497  elunirab 2504  uniun 2509  unissb 2518  elintrab 2535  intun 2552  intpr 2553  dfiun2g 2576  iunss 2581  ssiun 2582  ssiin 2589  iunin2 2598  iinun2 2599  iundif2 2600  iunxun 2604  iinuni 2605  iununi 2606  iinpw 2607  dftr2 2672  intexrab 2722  ssext 2753  pweqb 2755  opabid 2799  pwin 2814  pwun 2818  rexxfr 2891  ordtri3or 2969  dflim2 3015  unisuc 3036  sucexb 3038  sucelon 3058  onzsl 3107  dflim4 3109  opelxp 3204  rexxp 3209  brinxp2 3221  weinxp 3223  inopab 3258  inxp 3259  dmun 3306  dmuni 3308  dm0rn0 3319  brres 3357  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  cnvun 3441  cnvin 3442  rnuni 3445  dminss 3448  imainss 3449  cnvxp 3450  rninxp 3468  resco 3486  rnco 3488  coass 3498  cnvpo 3508  cnvso 3509  funcnv 3543  funcnv3 3544  fncnv 3547  fun11 3548  funin 3552  imadif 3560  fint 3635  fin 3636  fores 3666  f1o2 3678  f1o3 3679  f1o4 3681  f1orn 3683  f11o 3697  imaiun 3849  isomin 3884  iinon 3895  dfrdg2 3918  dfoprab2 3976  dfopab2 4097  dfoprab3 4098  foprab2 4103  oarec 4180  erdmrn 4260  mapval2 4319  map0e 4326  elixp2 4333  elixp 4334  mapixp 4346  domen 4361  brsdom 4363  brdom2 4369  xpcomen 4419  xpassen 4421  pw2en 4426  brsdom2 4441  mapdom2 4474  xpmapenlem5 4480  fiint 4534  tz9.12lem3 4633  rankc1 4677  cp 4694  aceq1 4701  aceq2 4703  aceq3 4705  aceq5lem3 4709  ac6lem 4726  distrlem1pr 5099  ltexprlem1 5114  reclem2pr 5129  gt0srpr 5159  ltpsrpr 5191  subsub23 5346  negcon2 5380  leadd1 5566  lesubadd 5569  leneg 5578  lesub0 5586  ltreci 5826  sup3 5999  xrsupss 6025  elnn0z 6094  elnn0nn 6118  nnwof 6391  discrlem1 6586  nn0opthlem1 6594  sqrlem16 6618  crrecz 6672  cvganz 6861  infcvglem1 7156  infxpidmlem7 7501  infmap2lem1 7521  istps2 7549  isbasis2g 7554  tgval2t 7559  basgent 7582  ntreq0 7650  pilem1 8590  cosh111lem3 8631  efifolem2 8638  axgroth3 8718  grothprim 8722  h2hlm 8789  choc0 9205  chcon2 9302  chcon1 9303  chcon3 9304  chnle 9323  cmcm2 9453  cmcm3 9454  3oalem3 9526  pjdifnorm 9545  pjnel 9585  dfadj2 9729  cnvadj 9733  eleigvec2t 9798  nmop0 9826  nmfn0 9827  nmcopexlem1 9866  nmcfnexlem1 9895  rnbra 9953  pjima 10015  pjhmopidm 10020  cvnbtwn4t 10126  chrelat4 10208  cbvrexf 10338  ntunte 10340  cmpdom 10364

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