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  4210  eqvinop  4383  pwexb  4620  dmun  4988  reldm0  4999  dmres  5084  imadmrn  5136  ssrnres  5230  dmsnm  5253  coundi  5289  coundir  5290  cnvpom  5330  xpcom  5334  fun11  5448  fununi  5449  funcnvuni  5450  isarep1  5467  fsn  5880  fconstfvm  5933  eufnfv  5949  fdmrn  6034  acexmidlem2  6082  eloprabga  6175  funoprabg  6187  ralrnmpo  6203  rexrnmpo  6204  oprabrexex2  6363  dfer2  6808  euen1b  7090  xpsnen  7119  rexuz3  11770  ballotfilem2  13277  ballotfilemi1  13294  imasaddfnlemg  13684  subsubrng2  14572  subsubrg2  14603  tgval2  15201  ssntr  15272  metrest  15656  plyun0  15886  sinhalfpilem  15942  2lgslem4  16320  wlkeq  16693  clwwlkn1  16757  clwwlkn2  16760  clwwlknon2x  16774