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  693  pm4.15  695  3or6  1335  sbal1yz  2028  2exsb  2036  moanim  2127  2eu4  2146  cvjust  2199  abbi  2318  sbc8g  3005  ss2rab  3268  unass  3329  unss  3346  undi  3420  difindiss  3426  notm0  3480  disj  3508  unopab  4122  eqvinop  4286  pwexb  4519  dmun  4883  reldm0  4894  dmres  4977  imadmrn  5029  ssrnres  5122  dmsnm  5145  coundi  5181  coundir  5182  cnvpom  5222  xpcom  5226  fun11  5335  fununi  5336  funcnvuni  5337  isarep1  5354  fsn  5746  fconstfvm  5792  eufnfv  5805  acexmidlem2  5931  eloprabga  6022  funoprabg  6034  ralrnmpo  6050  rexrnmpo  6051  oprabrexex2  6205  dfer2  6611  euen1b  6880  xpsnen  6898  rexuz3  11220  imasaddfnlemg  13064  subsubrng2  13895  subsubrg2  13926  tgval2  14441  ssntr  14512  metrest  14896  plyun0  15126  sinhalfpilem  15181  2lgslem4  15498