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  857  excxor  1423  sbequ8  1895  2sb5  2036  2sb6  2037  2sb5rf  2042  2sb6rf  2043  moabs  2129  moanim  2154  2eu4  2173  2eu7  2174  sb8ab  2354  risset  2561  cbvreuvw  2774  reuind  3012  difundi  3461  indifdir  3465  unab  3476  inab  3477  rabeq0  3526  abeq0  3527  inssdif0im  3564  snprc  3738  snssOLD  3803  unipr  3912  uni0b  3923  pwtr  4317  opm  4332  onintexmid  4677  elxp2  4749  opthprc  4783  xpiundir  4791  elvvv  4795  relun  4850  inopab  4868  difopab  4869  ralxpf  4882  rexxpf  4883  dmiun  4946  rniun  5154  cnvresima  5233  imaco  5249  fnopabg  5463  dff1o2  5597  idref  5907  imaiun  5911  opabex3d  6292  opabex3  6293  onntri35  7498  elixx3g  10179  elfz2  10293  elfzuzb  10297  divalgb  12547  1nprm  12747  issubg3  13840  cnfldui  14665  alsconv  16803