Theorem bitr2i 184

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr2i.1	⊢ (𝜑 ↔ 𝜓)
bitr2i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr2i	⊢ (𝜒 ↔ 𝜑)

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2i.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	bitri 183	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 131	1 ⊢ (𝜒 ↔ 𝜑)

Syntax hints:   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3bitrri  206  3bitr2ri  208  3bitr4ri  212  nan  662  pm4.15  828  3or6  1260  sbal1yz  1926  2exsb  1934  moanim  2023  2eu4  2042  cvjust  2084  abbi  2202  sbc8g  2848  ss2rab  3098  unass  3158  unss  3175  undi  3248  difindiss  3254  notm0  3307  disj  3335  unopab  3923  eqvinop  4079  pwexb  4309  dmun  4656  reldm0  4667  dmres  4747  imadmrn  4797  ssrnres  4886  dmsnm  4909  coundi  4945  coundir  4946  cnvpom  4986  xpcom  4990  fun11  5094  fununi  5095  funcnvuni  5096  isarep1  5113  fsn  5483  fconstfvm  5529  eufnfv  5539  acexmidlem2  5663  eloprabga  5749  funoprabg  5758  ralrnmpt2  5773  rexrnmpt2  5774  oprabrexex2  5915  dfer2  6307  euen1b  6574  xpsnen  6591  rexuz3  10484  tgval2  11812  ssntr  11883