Theorem 3bitr4 158

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	⊢ (φ ↔ ψ)
3bitr4.2	⊢ (χ ↔ φ)
3bitr4.3	⊢ (θ ↔ ψ)

Assertion

Ref	Expression
3bitr4	⊢ (χ ↔ θ)

Proof of Theorem 3bitr4

Step	Hyp	Ref	Expression
1		3bitr4.2	. 2 ⊢ (χ ↔ φ)
2		3bitr4.1	. . 3 ⊢ (φ ↔ ψ)
3		3bitr4.3	. . 3 ⊢ (θ ↔ ψ)
4	2, 3	bitr4 154	. 2 ⊢ (φ ↔ θ)
5	1, 4	bitr 151	1 ⊢ (χ ↔ θ)

Syntax hints:   ↔ wb 127

This theorem is referenced by:  orcom 209  orbi2i 214  or12 217  orass 218  or23 219  or4 220  anass 336  an23 371  an4 388  bicom 398  pm4.11 400  bicon2 403  ordir 453  jcab 454  andi 456  andir 457  pm5.32ri 490  biass 511  biluk 512  3anrot 586  3orrot 587  3ancoma 588  bi3an 606  bi3or 607  19.30 764  19.32 765  19.31 766  19.43 767  19.41 774  19.42 775  eqsex 834  cbvex 849  sbor 887  sban 889  sbbi 890  sb8e 919  eeeanv 981  sbel2x 995  sbex 998  sb8eu 1017  eu1 1019  cbvmo 1034  moanim 1051  euanv 1053  2eu4 1070  cleqcom 1103  cleqabr 1175  clelab 1187  sbabel 1189  necom 1198  ralnex 1209  rexnal 1210  birex2 1227  birala 1228  r2al 1231  r3al 1240  r2ex 1241  r19.21v 1260  r19.26 1289  r19.32v 1297  r19.41v 1302  r19.42v 1303  r19.43 1304  ralcom 1312  rexcom 1313  reeanv 1316  bireua 1319  cbvralf 1330  cbvrex 1332  cbvreuv 1335  reu2 1338  reu5 1339  eueq 1427  eqss 1516  dfpss3 1558  uncom 1604  unass 1615  ssequn1 1628  incom 1636  inass 1650  nssinpss 1665  nsspssun 1666  dfss4 1667  dfun2 1668  dfin2 1669  indi 1676  undi 1677  unab 1691  inab 1692  difab 1693  rabn0 1716  disj2 1735  disj3 1736  ssdif0 1748  difin0ss 1753  inssdif0 1754  snprc 1838  ssext 1865  pweqb 1867  pwin 1915  pwun 1918  eluni2 1923  uniun 1934  unissb 1941  elintrab 1977  intexrab 1988  intun 1989  intpr 1990  dfiun2 2014  iunss 2017  ssiun 2018  ssiin 2024  iunin2 2030  iinun2 2031  iundif2 2032  iunxun 2035  iinuni 2036  iununi 2037  iinpw 2038  dftr2 2043  opabid 2099  ordtri3or 2230  dflim2 2280  unisuc 2299  sucexb 2301  sucelon 2319  onzsl 2367  opelxp 2452  weinxp 2467  cbvop 2473  inopab 2495  inxp 2496  brcnv 2519  dmun 2536  dmuni 2538  dm0rn0 2549  cnvun 2642  cnvin 2643  rnuni 2646  dminss 2648  imainss 2649  imaiun 2650  cnvxp 2651  cores 2659  coass 2667  dmco2 2673  funcnv 2703  funin 2708  imadif 2714  fint 2769  fin 2770  fores 2794  f1o2 2804  f1o3 2805  f1o4 2807  f1orn 2809  f11o 2821  isomin 2937  iinon 2948  dfoprab2 3021  erdmrn 3213  map0e 3266  domen 3284  brsdom 3286  brdom2 3292  xpcomen 3343  xpassen 3344  pw2en 3348  brsdom2 3363  mapdom2 3389  xpmapenlem5 3395  tz9.12lem3 3505  cp 3547  aceq1 3552  aceq3 3556  aceq5lem3 3560  ac6lem 3575  kmlem4 3583  distrlem1pr 3921  ltexprlem1 3936  reclem2pr 3951  gt0srpr 3981  ltpsrpr 4013  subsub 4144  negcon2 4166  leadd1 4314  lesubadd2 4318  leneg 4331  lesub0 4341  negne0 4379  ltreci 4409  sup3 4511  elnn0z 4574  elnn0nn 4593  nnwof 4609  zmin 4617  discrlem1 4713  nn0opthlem1 4722  sqrlem16 4746  abslem2i 4866  infxpidmlem7 4939  infmap2lem1 4951  bcs 5101  choc0 5291  chcon2 5386  chcon3 5387  chnle 5406  h1det 5455  cmcm2 5502  cmcm3 5503  3oalem3 5554  pjdifnorm 5574  pjnel 5665  cvnbtwn4t 5721

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org