Theorem bitr2i 184

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

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  682  pm4.15  684  3or6  1305  sbal1yz  1981  2exsb  1989  moanim  2080  2eu4  2099  cvjust  2152  abbi  2271  sbc8g  2944  ss2rab  3204  unass  3264  unss  3281  undi  3355  difindiss  3361  notm0  3414  disj  3442  unopab  4043  eqvinop  4203  pwexb  4434  dmun  4793  reldm0  4804  dmres  4887  imadmrn  4938  ssrnres  5028  dmsnm  5051  coundi  5087  coundir  5088  cnvpom  5128  xpcom  5132  fun11  5237  fununi  5238  funcnvuni  5239  isarep1  5256  fsn  5639  fconstfvm  5685  eufnfv  5697  acexmidlem2  5821  eloprabga  5908  funoprabg  5920  ralrnmpo  5935  rexrnmpo  5936  oprabrexex2  6078  dfer2  6481  euen1b  6748  xpsnen  6766  rexuz3  10890  tgval2  12462  ssntr  12533  metrest  12917  sinhalfpilem  13123