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  693  pm4.15  695  3or6  1334  sbal1yz  2020  2exsb  2028  moanim  2119  2eu4  2138  cvjust  2191  abbi  2310  sbc8g  2997  ss2rab  3260  unass  3321  unss  3338  undi  3412  difindiss  3418  notm0  3472  disj  3500  unopab  4113  eqvinop  4277  pwexb  4510  dmun  4874  reldm0  4885  dmres  4968  imadmrn  5020  ssrnres  5113  dmsnm  5136  coundi  5172  coundir  5173  cnvpom  5213  xpcom  5217  fun11  5326  fununi  5327  funcnvuni  5328  isarep1  5345  fsn  5737  fconstfvm  5783  eufnfv  5796  acexmidlem2  5922  eloprabga  6013  funoprabg  6025  ralrnmpo  6041  rexrnmpo  6042  oprabrexex2  6196  dfer2  6602  euen1b  6871  xpsnen  6889  rexuz3  11172  imasaddfnlemg  13016  subsubrng2  13847  subsubrg2  13878  tgval2  14371  ssntr  14442  metrest  14826  plyun0  15056  sinhalfpilem  15111  2lgslem4  15428