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  2057  2exsb  2065  moanim  2157  2eu4  2176  cvjust  2229  abbibcom  2348  sbc8g  3053  ss2rab  3318  unass  3380  unss  3397  undi  3473  difindiss  3479  notm0  3533  disj  3561  unopab  4194  eqvinop  4364  pwexb  4600  dmun  4968  reldm0  4979  dmres  5064  imadmrn  5116  ssrnres  5210  dmsnm  5233  coundi  5269  coundir  5270  cnvpom  5310  xpcom  5314  fun11  5428  fununi  5429  funcnvuni  5430  isarep1  5447  fsn  5854  fconstfvm  5907  eufnfv  5922  fdmrn  6007  acexmidlem2  6055  eloprabga  6148  funoprabg  6160  ralrnmpo  6176  rexrnmpo  6177  oprabrexex2  6336  dfer2  6781  euen1b  7056  xpsnen  7085  rexuz3  11700  ballotfilem2  13172  ballotfilemi1  13189  imasaddfnlemg  13578  subsubrng2  14461  subsubrg2  14492  tgval2  15042  ssntr  15113  metrest  15497  plyun0  15727  sinhalfpilem  15782  2lgslem4  16102  wlkeq  16475  clwwlkn1  16539  clwwlkn2  16542  clwwlknon2x  16556