Theorem bitr3i 186

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
bitr3i.1	|- ( ps <-> ph )
bitr3i.2	|- ( ps <-> ch )

Assertion

Ref	Expression
bitr3i	|- ( ph <-> ch )

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 |- ( ps <-> ph )
2	1	bicomi 132	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 184	1 |- ( ph <-> ch )

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  3bitr3i  210  3bitr3ri  211  anandi  590  anandir  591  xchnxbi  681  orordi  774  orordir  775  sbco3v  1985  sbco4  2023  elsb1  2171  elsb2  2172  abeq1i  2305  cbvabw  2316  r19.41  2649  rexcom4a  2784  moeq  2936  mosubt  2938  2reuswapdc  2965  nfcdeq  2983  sbcid  3002  sbcco2  3009  sbc7  3013  sbcie2g  3020  eqsbc1  3026  sbcralt  3063  sbcrext  3064  cbvralcsf  3144  cbvrexcsf  3145  cbvrabcsf  3147  abss  3249  ssab  3250  difrab  3434  abn0m  3473  prsspw  3792  disjnim  4021  brab1  4077  unopab  4109  exss  4257  uniuni  4483  elvvv  4723  eliunxp  4802  ralxp  4806  rexxp  4807  opelco  4835  reldm0  4881  resieq  4953  resiexg  4988  iss  4989  imai  5022  cnvsym  5050  intasym  5051  asymref  5052  codir  5055  poirr2  5059  rninxp  5110  cnvsom  5210  funopg  5289  fin  5441  f1cnvcnv  5471  fndmin  5666  resoprab  6015  mpo2eqb  6029  ov6g  6058  offval  6140  dfopab2  6244  dfoprab3s  6245  fmpox  6255  spc2ed  6288  brtpos0  6307  dftpos3  6317  tpostpos  6319  ercnv  6610  xpcomco  6882  xpassen  6886  phpm  6923  ctssdccl  7172  elni2  7376  elfz2nn0  10181  elfzmlbp  10201  clim0  11431  nnwosdc  12179  isstructim  12635  xpscf  12933  srgrmhm  13493  ntreq0  14311  cnmptcom  14477  dedekindicclemicc  14811