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 485  an4 506  bicom 520  pm4.11 522  con2bi 525  oranabs 582  ordir 597  jcab 598  andi 604  andir 605  pm5.32ri 646  3anrot 780  3orrot 781  3ancoma 782  3anbi123i 822  3orbi123i 823  19.30 1085  19.32 1086  19.31 1087  19.43 1088  19.41 1095  19.42 1096  equsex 1152  cbvex 1166  dfsb3 1226  sbor 1235  sban 1237  sbbi 1239  sb8e 1262  sb6 1267  eeeanv 1324  sbel2x 1345  sbex 1348  sb8eu 1390  eu1 1392  cbvmo 1408  moanim 1427  euan 1428  eqcom 1477  abeq1 1569  clelab 1581  sbabel 1584  ralnex 1653  rexnal 1654  ralbii2 1671  rexbii2 1672  r2al 1676  r3al 1690  r2ex 1691  r19.26 1750  r19.32v 1758  r19.41v 1763  r19.42v 1764  r19.43 1765  ralcom 1774  rexcom 1775  reeanv 1778  reubiia 1781  cbvralf 1796  cbvrexf 1797  cbvrex 1799  cbvreuv 1802  eueq 1916  reu5 1929  reu2 1930  reu3 1931  reu6 1932  rmo4 1933  eqss 2077  dfpss3 2134  uncom 2176  unass 2187  ssequn1 2200  incom 2208  inass 2223  nssinpss 2240  nsspssun 2241  dfss4 2242  dfun2 2243  dfin2 2244  indi 2251  undi 2252  unab 2267  inab 2268  difab 2269  ne0f 2287  rabn0 2292  disj3 2314  ssdif0 2327  difin0ss 2332  inssdif0 2333  ssundif 2344  dfif2 2363  rexpr 2429  snprc 2443  r19.12sn 2444  eluni2 2507  elunirab 2514  uniun 2519  unissb 2528  elintrab 2545  intun 2562  intpr 2563  dfiun2g 2586  iunss 2591  ssiun 2592  ssiin 2599  iunin2 2608  iinun2 2609  iundif2 2610  iunxun 2614  iinuni 2615  iununi 2616  iinpw 2617  dftr2 2682  intexrab 2732  ssext 2763  pweqb 2765  opabid 2810  pwin 2825  pwun 2829  rexxfr 2901  dflim2 3025  unisuc 3046  sucexb 3048  sucelon 3068  onzsl 3117  dflim4 3119  opelxp 3214  rexxp 3219  brinxp2 3231  weinxp 3233  inopab 3268  inxp 3269  dmun 3317  dmuni 3319  dm0rn0 3330  brres 3373  asymref 3439  asymref2 3440  cnvun 3455  cnvin 3456  rnuni 3459  dminss 3462  imainss 3463  cnvxp 3464  rninxp 3482  resco 3500  rnco 3502  coass 3512  cnvpo 3522  cnvso 3523  funcnv 3557  funcnv3 3558  fncnv 3561  fun11 3562  funin 3566  imadif 3574  fint 3650  fin 3651  fores 3681  f1o2 3693  f1o3 3694  f1o4 3696  f1orn 3698  f11o 3712  imaiun 3864  isomin 3899  iinon 3910  dfrdg2 3933  dfoprab2 3991  dfopab2 4113  dfoprab3 4114  foprab2 4119  oarec 4196  erdmrn 4276  mapval2 4335  map0e 4342  elixp2 4349  elixp 4350  mapixp 4362  domen 4379  brsdom 4381  brdom2 4388  xpcomen 4439  xpassen 4441  pw2en 4446  brsdom2 4461  mapdom2 4494  xpmapenlem5 4500  fiint 4559  fiintOLD 4560  tz9.12lem3 4661  rankc1 4705  cp 4722  aceq1 4729  aceq2 4731  aceq3 4733  aceq5lem3 4737  ac6lem 4754  distrlem1pr 5127  ltexprlem1 5142  reclem2pr 5157  gt0srpr 5187  ltpsrpr 5219  subsub23 5374  negcon2 5408  leadd1 5592  lesubadd 5595  leneg 5604  lesub0 5612  ltreci 5878  sup3 6052  xrsupss 6078  elnn0z 6147  elnn0nn 6171  nnwof 6459  discrlem1 6656  nn0opthlem1 6664  sqrlem16 6688  crrecz 6741  cvganz 6924  infcvglem1 7221  infxpidmlem7 7558  infmap2lem1 7579  istps2 7607  isbasis2g 7612  tgval2t 7617  basgent 7640  ntreq0 7708  pilem1 8671  cosh111lem3 8716  efifolem2 8723  axgroth3 8779  grothprim 8783  h2hlm 8850  choc0 9290  chcon2 9387  chcon1 9388  chcon3 9389  chnle 9408  cmcm2 9536  cmcm3 9537  3oalem3 9609  pjdifnorm 9628  pjnel 9668  dfadj2 9812  cnvadj 9816  eleigvec2t 9882  nmop0 9910  nmfn0 9911  nmcopexlem1 9951  nmcfnexlem1 9980  rnbra 10040  pjima 10104  pjhmopidm 10110  cvnbtwn4t 10216  chrelat4 10300  ntunte 10439  cmpdom 10468

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