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  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  3572  unopab  4205  eqvinop  4378  pwexb  4615  dmun  4983  reldm0  4994  dmres  5079  imadmrn  5131  ssrnres  5225  dmsnm  5248  coundi  5284  coundir  5285  cnvpom  5325  xpcom  5329  fun11  5443  fununi  5444  funcnvuni  5445  isarep1  5462  fsn  5871  fconstfvm  5924  eufnfv  5939  fdmrn  6024  acexmidlem2  6072  eloprabga  6165  funoprabg  6177  ralrnmpo  6193  rexrnmpo  6194  oprabrexex2  6353  dfer2  6798  euen1b  7080  xpsnen  7109  rexuz3  11734  ballotfilem2  13206  ballotfilemi1  13223  imasaddfnlemg  13612  subsubrng2  14496  subsubrg2  14527  tgval2  15075  ssntr  15146  metrest  15530  plyun0  15760  sinhalfpilem  15815  2lgslem4  16136  wlkeq  16509  clwwlkn1  16573  clwwlkn2  16576  clwwlknon2x  16590