Theorem bitr2i 174

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 173	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 123	1 ⊢ (𝜒 ↔ 𝜑)

Syntax hints:   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  3bitrri  196  3bitr2ri  198  3bitr4ri  202  nan  626  pm4.15  789  3or6  1218  sbal1yz  1877  2exsb  1885  moanim  1974  2eu4  1993  cvjust  2035  abbi  2151  sbc8g  2771  ss2rab  3016  unass  3100  unss  3117  undi  3185  difindiss  3191  disj  3268  unopab  3836  eqvinop  3980  pwexb  4206  dmun  4542  reldm0  4553  dmres  4632  imadmrn  4678  ssrnres  4763  dmsnm  4786  coundi  4822  coundir  4823  cnvpom  4860  xpcom  4864  fun11  4966  fununi  4967  funcnvuni  4968  isarep1  4985  fsn  5335  fconstfvm  5379  eufnfv  5389  acexmidlem2  5509  eloprabga  5591  funoprabg  5600  ralrnmpt2  5615  rexrnmpt2  5616  oprabrexex2  5757  dfer2  6107  euen1b  6283  xpsnen  6295  rexuz3  9588