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  11756  ballotfilem2  13228  ballotfilemi1  13245  imasaddfnlemg  13635  subsubrng2  14523  subsubrg2  14554  tgval2  15152  ssntr  15223  metrest  15607  plyun0  15837  sinhalfpilem  15892  2lgslem4  16222  wlkeq  16595  clwwlkn1  16659  clwwlkn2  16662  clwwlknon2x  16676