Theorem bitr2i 183

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 182	. 2 |- ( ph <-> ch )
4	3	bicomi 130	1 |- ( ch <-> ph )

Syntax hints:   <-> wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3bitrri  205  3bitr2ri  207  3bitr4ri  211  nan  658  pm4.15  822  3or6  1254  sbal1yz  1918  2exsb  1926  moanim  2015  2eu4  2034  cvjust  2076  abbi  2192  sbc8g  2822  ss2rab  3070  unass  3129  unss  3146  undi  3212  difindiss  3218  disj  3292  unopab  3857  eqvinop  3998  pwexb  4224  dmun  4560  reldm0  4571  dmres  4650  imadmrn  4698  ssrnres  4783  dmsnm  4806  coundi  4842  coundir  4843  cnvpom  4880  xpcom  4884  fun11  4986  fununi  4987  funcnvuni  4988  isarep1  5005  fsn  5356  fconstfvm  5400  eufnfv  5410  acexmidlem2  5529  eloprabga  5611  funoprabg  5620  ralrnmpt2  5635  rexrnmpt2  5636  oprabrexex2  5777  dfer2  6130  euen1b  6306  xpsnen  6318  rexuz3  9876