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  1334  sbal1yz  2020  2exsb  2028  moanim  2119  2eu4  2138  cvjust  2191  abbi  2310  sbc8g  2997  ss2rab  3259  unass  3320  unss  3337  undi  3411  difindiss  3417  notm0  3471  disj  3499  unopab  4112  eqvinop  4276  pwexb  4509  dmun  4873  reldm0  4884  dmres  4967  imadmrn  5019  ssrnres  5112  dmsnm  5135  coundi  5171  coundir  5172  cnvpom  5212  xpcom  5216  fun11  5325  fununi  5326  funcnvuni  5327  isarep1  5344  fsn  5734  fconstfvm  5780  eufnfv  5793  acexmidlem2  5919  eloprabga  6009  funoprabg  6021  ralrnmpo  6037  rexrnmpo  6038  oprabrexex2  6187  dfer2  6593  euen1b  6862  xpsnen  6880  rexuz3  11155  imasaddfnlemg  12957  subsubrng2  13771  subsubrg2  13802  tgval2  14287  ssntr  14358  metrest  14742  plyun0  14972  sinhalfpilem  15027  2lgslem4  15344