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  692  pm4.15  694  3or6  1323  sbal1yz  2001  2exsb  2009  moanim  2100  2eu4  2119  cvjust  2172  abbi  2291  sbc8g  2971  ss2rab  3232  unass  3293  unss  3310  undi  3384  difindiss  3390  notm0  3444  disj  3472  unopab  4083  eqvinop  4244  pwexb  4475  dmun  4835  reldm0  4846  dmres  4929  imadmrn  4981  ssrnres  5072  dmsnm  5095  coundi  5131  coundir  5132  cnvpom  5172  xpcom  5176  fun11  5284  fununi  5285  funcnvuni  5286  isarep1  5303  fsn  5689  fconstfvm  5735  eufnfv  5748  acexmidlem2  5872  eloprabga  5962  funoprabg  5974  ralrnmpo  5989  rexrnmpo  5990  oprabrexex2  6131  dfer2  6536  euen1b  6803  xpsnen  6821  rexuz3  10999  imasaddfnlemg  12735  subsubrg2  13367  tgval2  13554  ssntr  13625  metrest  14009  sinhalfpilem  14215