Theorem bitr2i 241

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 240	. 2 ⊢ (φ ↔ χ)
4	3	bicomi 193	1 ⊢ (χ ↔ φ)

Syntax hints:   ↔ wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  3bitrri  263  3bitr2ri  265  3bitr4ri  269  nan  563  pm4.15  564  pm5.17  858  pm4.83  895  pm5.7  900  3or6  1263  nanim  1292  hadnot  1393  19.12vv  1898  2exsb  2132  2eu4  2287  cvjust  2348  abbi  2463  spc3gv  2944  sbc8g  3053  ss2rab  3342  difdif  3392  ddif  3398  unass  3420  unss  3437  undi  3502  rabeq0  3572  disj  3591  ssindif0  3604  pwsnALT  3882  dfpss4  3888  iinrab2  4029  imacok  4282  dfaddc2  4381  dfnnc2  4395  nnsucelr  4428  tfinnn  4534  eqvinop  4606  unopab  4638  elswap  4740  dfswap2  4741  ssrnres  5059  cnvresima  5077  coundi  5082  coundir  5083  coass  5097  fun11  5159  fununi  5160  funcnvuni  5161  fsn  5432  fconstfv  5456  eloprabga  5578  funoprabg  5583  releqmpt2  5809  funsex  5828  brpprod  5839  fvfullfunlem1  5861  enpw1lem1  6061  enpw1pw  6075  lecex  6115  nncdiv3lem1  6275  nchoicelem11  6299