Theorem bitr2i 185

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

Syntax hints:   <-> wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3bitrri  207  3bitr2ri  209  3bitr4ri  213  nan  698  pm4.15  701  3or6  1359  sbal1yz  2054  2exsb  2062  moanim  2154  2eu4  2173  cvjust  2226  abbi  2345  sbc8g  3039  ss2rab  3303  unass  3364  unss  3381  undi  3455  difindiss  3461  notm0  3515  disj  3543  unopab  4168  eqvinop  4335  pwexb  4571  dmun  4938  reldm0  4949  dmres  5034  imadmrn  5086  ssrnres  5179  dmsnm  5202  coundi  5238  coundir  5239  cnvpom  5279  xpcom  5283  fun11  5397  fununi  5398  funcnvuni  5399  isarep1  5416  fsn  5819  fconstfvm  5872  eufnfv  5885  acexmidlem2  6015  eloprabga  6108  funoprabg  6120  ralrnmpo  6136  rexrnmpo  6137  oprabrexex2  6292  dfer2  6703  euen1b  6977  xpsnen  7005  rexuz3  11568  imasaddfnlemg  13415  subsubrng2  14248  subsubrg2  14279  tgval2  14794  ssntr  14865  metrest  15249  plyun0  15479  sinhalfpilem  15534  2lgslem4  15851  wlkeq  16224  clwwlkn1  16288  clwwlkn2  16291  clwwlknon2x  16305