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  681  pm4.15  683  3or6  1301  sbal1yz  1974  2exsb  1982  moanim  2071  2eu4  2090  cvjust  2132  abbi  2251  sbc8g  2911  ss2rab  3168  unass  3228  unss  3245  undi  3319  difindiss  3325  notm0  3378  disj  3406  unopab  4002  eqvinop  4160  pwexb  4390  dmun  4741  reldm0  4752  dmres  4835  imadmrn  4886  ssrnres  4976  dmsnm  4999  coundi  5035  coundir  5036  cnvpom  5076  xpcom  5080  fun11  5185  fununi  5186  funcnvuni  5187  isarep1  5204  fsn  5585  fconstfvm  5631  eufnfv  5641  acexmidlem2  5764  eloprabga  5851  funoprabg  5863  ralrnmpo  5878  rexrnmpo  5879  oprabrexex2  6021  dfer2  6423  euen1b  6690  xpsnen  6708  rexuz3  10755  tgval2  12209  ssntr  12280  metrest  12664  sinhalfpilem  12861