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  6812  euen1b  7094  xpsnen  7123  rexuz3  11778  ballotfilem2  13286  ballotfilemi1  13303  imasaddfnlemg  13694  subsubrng2  14632  subsubrg2  14663  tgval2  15274  ssntr  15345  metrest  15729  plyun0  15959  sinhalfpilem  16015  2lgslem4  16424  wlkeq  16797  clwwlkn1  16861  clwwlkn2  16864  clwwlknon2x  16878