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 )

This proof depends on syntax axioms:   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3bitrri  207  3bitr2ri  209  3bitr4ri  213  nan  703  pm4.15  706  3or6  1364  sbal1yz  2061  2exsb  2069  moanim  2161  2eu4  2180  cvjust  2233  abbibcom  2352  sbc8g  3059  ss2rab  3324  unass  3386  unss  3403  undi  3479  difindiss  3485  notm0  3542  disj  3573  unopab  4211  eqvinop  4385  pwexb  4622  dmun  4990  reldm0  5001  dmres  5086  imadmrn  5139  ssrnres  5233  dmsnm  5256  coundi  5292  coundir  5293  cnvpom  5333  xpcom  5337  fun11  5451  fununi  5452  funcnvuni  5453  isarep1  5470  fsn  5883  fconstfvm  5936  eufnfv  5952  fdmrn  6037  acexmidlem2  6085  eloprabga  6178  funoprabg  6190  ralrnmpo  6206  rexrnmpo  6207  oprabrexex2  6367  dfer2  6813  euen1b  7096  xpsnen  7125  rexuz3  11777  ballotfilem2  13285  ballotfilemi1  13302  imasaddfnlemg  13693  subsubrng2  14631  subsubrg2  14662  tgval2  15294  ssntr  15365  metrest  15749  plyun0  15979  sinhalfpilem  16035  2lgslem4  16444  wlkeq  16817  clwwlkn1  16881  clwwlkn2  16884  clwwlknon2x  16898