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  682  orordi  775  orordir  776  sbco3v  1998  sbco4  2036  elsb1  2184  elsb2  2185  abeq1i  2318  cbvabw  2329  r19.41  2662  rexcom4a  2798  moeq  2952  mosubt  2954  2reuswapdc  2981  nfcdeq  2999  sbcid  3018  sbcco2  3025  sbc7  3029  sbcie2g  3036  eqsbc1  3042  sbcralt  3079  sbcrext  3080  cbvralcsf  3160  cbvrexcsf  3161  cbvrabcsf  3163  abss  3266  ssab  3267  difrab  3451  abn0m  3490  prsspw  3812  disjnim  4041  brab1  4099  unopab  4131  exss  4279  uniuni  4506  elvvv  4746  eliunxp  4825  ralxp  4829  rexxp  4830  opelco  4858  reldm0  4905  resieq  4978  resiexg  5013  iss  5014  imai  5047  cnvsym  5075  intasym  5076  asymref  5077  codir  5080  poirr2  5084  rninxp  5135  cnvsom  5235  funopg  5314  fin  5474  f1cnvcnv  5504  fndmin  5700  resoprab  6054  mpo2eqb  6068  ov6g  6097  offval  6179  dfopab2  6288  dfoprab3s  6289  fmpox  6299  spc2ed  6332  brtpos0  6351  dftpos3  6361  tpostpos  6363  ercnv  6654  xpcomco  6936  xpassen  6940  phpm  6977  ctssdccl  7228  elni2  7447  elfz2nn0  10254  elfzmlbp  10274  clim0  11671  nnwosdc  12435  isstructim  12921  xpscf  13254  srgrmhm  13831  ntreq0  14679  cnmptcom  14845  dedekindicclemicc  15179