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  694  pm4.15  696  3or6  1336  sbal1yz  2030  2exsb  2038  moanim  2129  2eu4  2148  cvjust  2201  abbi  2320  sbc8g  3010  ss2rab  3273  unass  3334  unss  3351  undi  3425  difindiss  3431  notm0  3485  disj  3513  unopab  4131  eqvinop  4295  pwexb  4529  dmun  4894  reldm0  4905  dmres  4989  imadmrn  5041  ssrnres  5134  dmsnm  5157  coundi  5193  coundir  5194  cnvpom  5234  xpcom  5238  fun11  5350  fununi  5351  funcnvuni  5352  isarep1  5369  fsn  5765  fconstfvm  5815  eufnfv  5828  acexmidlem2  5954  eloprabga  6045  funoprabg  6057  ralrnmpo  6073  rexrnmpo  6074  oprabrexex2  6228  dfer2  6634  euen1b  6908  xpsnen  6931  rexuz3  11376  imasaddfnlemg  13221  subsubrng2  14052  subsubrg2  14083  tgval2  14598  ssntr  14669  metrest  15053  plyun0  15283  sinhalfpilem  15338  2lgslem4  15655