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  2055  2exsb  2063  moanim  2155  2eu4  2174  cvjust  2227  abbibcom  2346  sbc8g  3050  ss2rab  3314  unass  3376  unss  3393  undi  3469  difindiss  3475  notm0  3529  disj  3557  unopab  4189  eqvinop  4359  pwexb  4595  dmun  4963  reldm0  4974  dmres  5059  imadmrn  5111  ssrnres  5205  dmsnm  5228  coundi  5264  coundir  5265  cnvpom  5305  xpcom  5309  fun11  5423  fununi  5424  funcnvuni  5425  isarep1  5442  fsn  5849  fconstfvm  5902  eufnfv  5917  acexmidlem2  6047  eloprabga  6140  funoprabg  6152  ralrnmpo  6168  rexrnmpo  6169  oprabrexex2  6323  dfer2  6768  euen1b  7043  xpsnen  7072  rexuz3  11675  ballotfilem2  13142  imasaddfnlemg  13527  subsubrng2  14360  subsubrg2  14391  tgval2  14916  ssntr  14987  metrest  15371  plyun0  15601  sinhalfpilem  15656  2lgslem4  15976  wlkeq  16349  clwwlkn1  16413  clwwlkn2  16416  clwwlknon2x  16430