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  699  pm4.15  702  3or6  1360  sbal1yz  2054  2exsb  2062  moanim  2154  2eu4  2173  cvjust  2226  abbi  2345  sbc8g  3040  ss2rab  3304  unass  3366  unss  3383  undi  3457  difindiss  3463  notm0  3517  disj  3545  unopab  4173  eqvinop  4341  pwexb  4577  dmun  4944  reldm0  4955  dmres  5040  imadmrn  5092  ssrnres  5186  dmsnm  5209  coundi  5245  coundir  5246  cnvpom  5286  xpcom  5290  fun11  5404  fununi  5405  funcnvuni  5406  isarep1  5423  fsn  5827  fconstfvm  5880  eufnfv  5895  acexmidlem2  6025  eloprabga  6118  funoprabg  6130  ralrnmpo  6146  rexrnmpo  6147  oprabrexex2  6301  dfer2  6746  euen1b  7020  xpsnen  7048  rexuz3  11613  imasaddfnlemg  13460  subsubrng2  14293  subsubrg2  14324  tgval2  14845  ssntr  14916  metrest  15300  plyun0  15530  sinhalfpilem  15585  2lgslem4  15905  wlkeq  16278  clwwlkn1  16342  clwwlkn2  16345  clwwlknon2x  16359