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  5871  eufnfv  5884  acexmidlem2  6014  eloprabga  6107  funoprabg  6119  ralrnmpo  6135  rexrnmpo  6136  oprabrexex2  6291  dfer2  6702  euen1b  6976  xpsnen  7004  rexuz3  11550  imasaddfnlemg  13396  subsubrng2  14228  subsubrg2  14259  tgval2  14774  ssntr  14845  metrest  15229  plyun0  15459  sinhalfpilem  15514  2lgslem4  15831  wlkeq  16204  clwwlkn1  16268  clwwlkn2  16271  clwwlknon2x  16285