Theorem bitr3i 251

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-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 202	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 249	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185

This theorem is referenced by:  3bitrri  272  3bitr3i  275  3bitr3ri  276  xchnxbi  308  ianor  488  orordi  530  orordir  531  anandi  824  anandir  825  trunantru  1411  falnanfal  1414  cadanOLD  1434  had0  1445  nic-axALT  1481  sbied  2102  sbidm  2109  sb6a  2155  sbelx  2168  sbco4  2179  mo  2300  2eu6  2371  2eu6OLD  2372  bm1.1  2427  abeq1iOLD  2557  cbvab  2568  necon1bbii  2687  r19.41  2893  2ralor  2911  rexcom4a  3014  moeq  3156  2reuswap  3182  2reu5  3188  nfcdeq  3204  sbcid  3224  sbcco2  3231  sbc7  3235  sbcie2g  3241  eqsbc3  3247  sbcralt  3288  cbvralcsf  3340  cbvrabcsf  3343  abss  3442  ssab  3443  difrab  3645  neq0  3668  sbccsb  3722  vdif0  3759  difrab0eq  3760  ssunsn2  4053  sspr  4057  sstp  4058  prsspw  4066  uniintsn  4186  disjmoOLD  4298  brab1  4358  unopab  4388  axrep5  4429  axsep  4433  intexab  4471  reusv2lem4  4517  reusv2  4519  reuxfrd  4538  wefrc  4735  ordelord  4762  elvvv  4919  eliunxp  4998  ralxp  5002  rexxp  5003  opelco  5032  reldm0  5078  resieq  5142  iss  5175  imai  5202  cnvsym  5233  intasym  5234  asymref  5235  codir  5239  poirr2  5243  xpdifid  5287  rninxp  5298  dffun3  5450  funopg  5471  fin  5612  f1cnvcnv  5635  funimass4  5763  fnressn  5915  resoprab  6207  mpt22eqb  6220  elrnmpt2res  6225  ov6g  6249  offval  6348  uniuni  6406  dfwe2  6414  orduniorsuc  6462  tfinds2  6495  resiexg  6535  dfopab2  6649  dfoprab3s  6650  fmpt2x  6661  fparlem1  6693  fparlem2  6694  brtpos0  6773  dftpos3  6784  tpostpos  6786  tz7.48lem  6917  omeu  7045  ercnv  7143  ixp0  7317  xpcomco  7422  xpassen  7426  php  7516  findcard3  7576  ixpfi2  7630  dfsup2  7713  card2on  7790  infeq5i  7863  cnfcom3lem  7957  cnfcom3lemOLD  7965  r1elss  8034  rankxplim  8107  scott0s  8116  aceq1  8308  dfac5lem1  8314  dfac5lem2  8315  kmlem3  8342  kmlem8  8347  kmlem16  8355  cflem  8436  cf0  8441  alephval2  8757  rankcf  8965  r1tskina  8970  wfgru  9004  genpass  9199  psslinpr  9221  ltpsrpr  9297  infm3  10310  nnwos  10943  ioo0  11346  ico0  11367  ioc0  11368  icc0  11369  elfz2nn0  11501  elfzmlbp  11512  sqeqori  11999  hashgt12el  12194  hashgt12el2  12195  cshwidxmod  12461  clim0  13005  dvdslelem  13598  divalglem6  13623  isprm2lem  13791  pceu  13934  prmreclem2  13999  cshwshash  14152  isstruct  14205  xpscf  14525  acsfn2  14622  invsym2  14722  pospo  15164  f1omvdco3  15976  psgnunilem5  16021  efgrelexlemb  16268  gexex  16356  srgrmhm  16657  lssne0  17054  opsrtoslem1  17587  opsrtoslem2  17588  islindf4  18289  mdetunilem8  18447  ntreq0  18703  ordtrest2lem  18829  ist0-3  18971  ist1-2  18973  ist1-3  18975  cmpfi  19033  2ndcctbss  19081  ptbasfi  19176  ptcnplem  19216  hausdiag  19240  hauseqlcld  19241  cnmptcom  19273  txflf  19601  tgphaus  19709  metrest  20121  iccpnfcnv  20538  bcth3  20864  volun  21048  dyadmax  21100  vitalilem2  21111  vitalilem3  21112  mbfimaopnlem  21155  itg2leub  21234  dvres2  21409  ellogdm  22106  reasinsin  22313  leibpilem2  22358  ftalem3  22434  dchreq  22619  axcontlem2  23233  lnon0  24220  spansncvi  25077  pjssmii  25106  nmlnopgt0i  25423  largei  25693  cvexchlem  25794  xfree  25870  nmo  25891  2reuswap2  25894  fpwrelmapffslem  26054  addeq0  26057  eliccioo  26128  omndmul2  26197  ordtrest2NEWlem  26374  ordtconlem1  26376  xrge0iifcnv  26385  xrge0iifiso  26387  xrge0iifhom  26389  cntnevol  26664  eulerpartlemgh  26783  ballotlemfp1  26896  ballotlem7  26940  signswch  26984  derang0  27079  iccllyscon  27161  cvmsss2  27185  axacprim  27380  dftr6  27582  dfpo2  27587  opelco3  27611  elima4  27612  setinds2f  27614  elpotr  27616  tz6.26  27688  wfis2fg  27694  frins2fg  27730  wzel  27783  nobndlem1  27855  elfuns  27968  dfiota3  27976  imagesset  28006  lineunray  28200  ellines  28205  hfninf  28246  finixpnum  28440  fin2so  28442  tan2h  28450  ovoliunnfl  28459  voliunnfl  28461  ftc1anc  28501  inixp  28648  heibor1lem  28734  sbccom2lem  28959  csbcom2fi  28964  tsna1  28981  4rexfrabdioph  29162  dford4  29404  isdomn3  29598  fgraphopab  29604  2rmoswap  30034  ndmaovcom  30137  rabasiun  30256  wlk0  30318  usgra2pth0  30328  rusgranumwlklem0  30592  frgra3v  30620  4cycl2vnunb  30635  vdn0frgrav2  30642  vdgn0frgrav2  30643  usg2spot2nb  30684  eliunxp2  30747  pgrpgt2nabel  30799  islindeps  30984  lindslinindsimp1  30988  lindslinindsimp2  30994  cnstpmatmcllem  31070  pmatcollpw2lem  31120  opelopab4  31356  2sb5nd  31365  un2122  31619  uunT12p4  31632  onfrALTlem5VD  31717  2sb5ndVD  31742  2sb5ndALT  31764  bnj446  31801  bnj563  31831  bnj110  31947  bnj153  31969  bnj557  31990  bnj864  32011  bnj865  32012  bnj849  32014  bnj929  32025  bnj1110  32069  bj-axrep5  32409  bj-axsep  32410  bj-rexcom4a  32477  bj-snglc  32558  islshpat  32758  lkr0f  32835  lshpsmreu  32850  cvrnbtwn4  33020  ishlat2  33094  islvol5  33319  tendoeq2  34514  dibelval3  34888  mapdpglem3  35416  hdmapglem7a  35671