Theorem 3bitr4ri 213

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4ri	⊢ (𝜃 ↔ 𝜒)

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 187	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitr2i 185	1 ⊢ (𝜃 ↔ 𝜒)

Syntax hints:   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dcnnOLD  851  excxor  1398  sbequ8  1871  2sb5  2012  2sb6  2013  2sb5rf  2018  2sb6rf  2019  moabs  2104  moanim  2129  2eu4  2148  2eu7  2149  sb8ab  2328  risset  2535  cbvreuvw  2745  reuind  2980  difundi  3427  indifdir  3431  unab  3442  inab  3443  rabeq0  3492  abeq0  3493  inssdif0im  3530  snprc  3700  snssOLD  3762  unipr  3867  uni0b  3878  pwtr  4268  opm  4283  onintexmid  4626  elxp2  4698  opthprc  4731  xpiundir  4739  elvvv  4743  relun  4797  inopab  4815  difopab  4816  ralxpf  4829  rexxpf  4830  dmiun  4893  rniun  5099  cnvresima  5178  imaco  5194  fnopabg  5406  dff1o2  5536  idref  5835  imaiun  5839  opabex3d  6216  opabex3  6217  onntri35  7362  elixx3g  10036  elfz2  10150  elfzuzb  10154  divalgb  12286  1nprm  12486  issubg3  13578  cnfldui  14401  alsconv  16134