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  1334  sbal1yz  2017  2exsb  2025  moanim  2116  2eu4  2135  cvjust  2188  abbi  2307  sbc8g  2993  ss2rab  3255  unass  3316  unss  3333  undi  3407  difindiss  3413  notm0  3467  disj  3495  unopab  4108  eqvinop  4272  pwexb  4505  dmun  4869  reldm0  4880  dmres  4963  imadmrn  5015  ssrnres  5108  dmsnm  5131  coundi  5167  coundir  5168  cnvpom  5208  xpcom  5212  fun11  5321  fununi  5322  funcnvuni  5323  isarep1  5340  fsn  5730  fconstfvm  5776  eufnfv  5789  acexmidlem2  5915  eloprabga  6005  funoprabg  6017  ralrnmpo  6033  rexrnmpo  6034  oprabrexex2  6182  dfer2  6588  euen1b  6857  xpsnen  6875  rexuz3  11134  imasaddfnlemg  12897  subsubrng2  13711  subsubrg2  13742  tgval2  14219  ssntr  14290  metrest  14674  plyun0  14882  sinhalfpilem  14926