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  693  pm4.15  695  3or6  1335  sbal1yz  2028  2exsb  2036  moanim  2127  2eu4  2146  cvjust  2199  abbi  2318  sbc8g  3005  ss2rab  3268  unass  3329  unss  3346  undi  3420  difindiss  3426  notm0  3480  disj  3508  unopab  4122  eqvinop  4286  pwexb  4520  dmun  4884  reldm0  4895  dmres  4979  imadmrn  5031  ssrnres  5124  dmsnm  5147  coundi  5183  coundir  5184  cnvpom  5224  xpcom  5228  fun11  5340  fununi  5341  funcnvuni  5342  isarep1  5359  fsn  5751  fconstfvm  5801  eufnfv  5814  acexmidlem2  5940  eloprabga  6031  funoprabg  6043  ralrnmpo  6059  rexrnmpo  6060  oprabrexex2  6214  dfer2  6620  euen1b  6894  xpsnen  6915  rexuz3  11243  imasaddfnlemg  13088  subsubrng2  13919  subsubrg2  13950  tgval2  14465  ssntr  14536  metrest  14920  plyun0  15150  sinhalfpilem  15205  2lgslem4  15522