Theorem bitr2i 241

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

Hypotheses

Ref	Expression
bitr2i.1	|- (ph <-> ps)
bitr2i.2	|- (ps <-> ch)

Assertion

Ref	Expression
bitr2i	|- (ch <-> ph)

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 |- (ph <-> ps)
2		bitr2i.2	. . 3 |- (ps <-> ch)
3	1, 2	bitri 240	. 2 |- (ph <-> ch)
4	3	bicomi 193	1 |- (ch <-> ph)

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  2464  spc3gv  2945  sbc8g  3054  ss2rab  3343  difdif  3393  ddif  3399  unass  3421  unss  3438  undi  3503  rabeq0  3573  disj  3592  ssindif0  3605  pwsnALT  3883  dfpss4  3889  iinrab2  4030  imacok  4283  dfaddc2  4382  dfnnc2  4396  nnsucelr  4429  tfinnn  4535  eqvinop  4607  unopab  4639  elswap  4741  dfswap2  4742  ssrnres  5060  cnvresima  5078  coundi  5083  coundir  5084  coass  5098  fun11  5160  fununi  5161  funcnvuni  5162  fsn  5433  fconstfv  5457  eloprabga  5579  funoprabg  5584  releqmpt2  5810  funsex  5829  brpprod  5840  fvfullfunlem1  5862  enpw1lem1  6062  enpw1pw  6076  lecex  6116  nncdiv3lem1  6276  nchoicelem11  6300