Theorem bitr3i 259

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 207	. 2 |- ( ph <-> ps )
3		bitr3i.2	. 2 |- ( ps <-> ch )
4	2, 3	bitri 257	1 |- ( ph <-> ch )

Syntax hints:   <-> wb 189

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 190

This theorem is referenced by:  3bitrri  280  3bitr3i  283  3bitr3ri  284  xchnxbi  315  ianor  496  orordi  539  orordir  540  anandi  844  anandir  845  trunantru  1494  falnanfal  1498  had0  1515  nic-axALT  1565  sbied  2258  sbidm  2263  sb6a  2297  sbelx  2307  sbco4  2315  mo  2357  2eu6  2407  bm1.1  2456  cbvab  2594  nabbi  2744  r19.41v  2928  r19.41  2929  2ralor  2946  rexcom4a  3054  moeq  3202  2reuswap  3230  2reu5  3236  nfcdeq  3252  sbcid  3272  sbcco2  3279  sbc7  3283  sbcie2g  3289  eqsbc3  3295  sbcralt  3328  cbvralcsf  3381  cbvrabcsf  3384  abss  3484  ssab  3485  difrab  3708  euelss  3721  neq0  3733  sbccsb  3797  vdif0  3827  difrab0eq  3828  ssunsn2  4123  sspr  4127  sstp  4128  uniintsn  4263  rabasiun  4273  brab1  4441  unopab  4471  axrep5  4513  axsep  4517  intexab  4559  reusv2lem4  4605  reusv2  4607  reuxfrd  4625  wefrc  4833  elvvv  4899  eliunxp  4977  ralxp  4981  rexxp  4982  opelco  5011  reldm0  5058  resieq  5121  iss  5158  imai  5186  cnvsym  5220  intasym  5221  asymref  5222  codir  5226  poirr2  5230  xpdifid  5271  rninxp  5282  tz6.26  5418  wfis2fg  5424  ordelord  5452  dffun3  5600  funopg  5621  fin  5776  f1cnvcnv  5800  funimass4  5930  fnressn  6092  resoprab  6411  mpt22eqb  6424  elrnmpt2res  6429  ov6g  6453  offval  6557  uniuni  6619  dfwe2  6627  orduniorsuc  6676  tfinds2  6709  resiexg  6748  dfopab2  6866  dfoprab3s  6867  fmpt2x  6878  fparlem1  6915  fparlem2  6916  brtpos0  6998  dftpos3  7009  tpostpos  7011  dfrecs3  7109  tz7.48lem  7176  omeu  7304  ercnv  7402  ixp0  7573  xpcomco  7680  xpassen  7684  php  7774  findcard3  7832  ixpfi2  7890  dfsup2  7976  sup0riota  7997  card2on  8087  infeq5i  8159  cnfcom3lem  8226  r1elss  8295  rankxplim  8368  scott0s  8377  aceq1  8566  dfac5lem1  8572  dfac5lem2  8573  kmlem3  8600  kmlem8  8605  kmlem16  8613  cflem  8694  cf0  8699  alephval2  9015  rankcf  9220  r1tskina  9225  wfgru  9259  genpass  9452  psslinpr  9474  ltpsrpr  9551  infm3  10590  nnwos  11249  ioo0  11686  ico0  11707  ioc0  11708  icc0  11709  elfz2nn0  11911  elfzmlbp  11927  sqeqori  12424  hashgt12el  12636  hashgt12el2  12637  cshwidxmod  12959  clim0  13647  divalglem6  14457  isprm2lem  14710  ncoprmlnprm  14756  pceu  14875  prmreclem2  14940  cshwshash  15153  isstruct  15209  xpscf  15550  acsfn2  15647  invsym2  15746  pospo  16297  f1omvdco3  17168  psgnunilem5  17213  efgrelexlemb  17478  gexex  17569  srgrmhm  17847  lssne0  18252  opsrtoslem1  18784  opsrtoslem2  18785  islindf4  19473  mdetunilem8  19721  cpmatmcllem  19819  pmatcollpw2lem  19878  ntreq0  20170  ordtrest2lem  20296  ist0-3  20438  ist1-2  20440  ist1-3  20442  cmpfi  20500  2ndcctbss  20547  ptbasfi  20673  ptcnplem  20713  hausdiag  20737  hauseqlcld  20738  cnmptcom  20770  txflf  21099  tgphaus  21209  metrest  21617  iccpnfcnv  22050  bcth3  22377  volun  22577  dyadmax  22635  vitalilem2  22646  vitalilem3  22647  mbfimaopnlem  22690  itg2leub  22771  dvres2  22946  ellogdm  23663  reasinsin  23901  leibpilem2  23946  ftalem3  24078  dchreq  24265  legso  24723  outpasch  24876  axcontlem2  25074  rusgranumwlklem0  25755  frgra3v  25809  4cycl2vnunb  25824  vdn0frgrav2  25830  vdgn0frgrav2  25831  usg2spot2nb  25872  lnon0  26520  spansncvi  27386  pjssmii  27415  nmlnopgt0i  27731  largei  28001  cvexchlem  28102  xfree  28178  spc2ed  28187  nmo  28200  2reuswap2  28203  fpwrelmapffslem  28392  addeq0  28395  eliccioo  28475  qtophaus  28737  ordtrest2NEWlem  28802  ordtconlem1  28804  xrge0iifcnv  28813  xrge0iifiso  28815  xrge0iifhom  28817  cntnevol  29124  eulerpartlemgh  29284  ballotlem7  29441  ballotlem7OLD  29479  signswch  29522  bnj446  29594  bnj563  29625  bnj110  29741  bnj153  29763  bnj864  29805  bnj865  29806  bnj849  29808  bnj929  29819  bnj1110  29863  derang0  29964  iccllyscon  30045  cvmsss2  30069  elmrsubrn  30230  quad3  30374  axacprim  30406  dftr6  30461  dfpo2  30466  opelco3  30491  elima4  30492  setinds2f  30496  elpotr  30498  frins2fg  30556  wzel  30578  nobndlem1  30652  elfuns  30753  dfiota3  30761  imagesset  30791  lineunray  30985  ellines  30990  hfninf  31024  bj-axrep5  31473  bj-axsep  31474  bj-rexcom4a  31547  bj-snglc  31633  bj-mpt2mptALT  31701  tan2h  32001  poimirlem26  32030  poimirlem27  32031  poimirlem30  32034  poimirlem32  32036  poimir  32037  ovoliunnfl  32046  voliunnfl  32048  ftc1anc  32089  inixp  32119  heibor1lem  32205  csbcom2fi  32433  tsna1  32450  islshpat  32654  lkr0f  32731  lshpsmreu  32746  cvrnbtwn4  32916  ishlat2  32990  islvol5  33215  tendoeq2  34412  dibelval3  34786  mapdpglem3  35314  hdmapglem7a  35569  4rexfrabdioph  35712  dford4  35955  isdomn3  36152  fgraphopab  36158  ifpim123g  36215  ifpbibib  36225  undmrnresiss  36281  cnvssco  36283  iunrelexpuztr  36382  dffrege115  36645  undisjrab  36724  radcnvrat  36733  opelopab4  36988  2sb5nd  36997  un2122  37240  uunT12p4  37253  onfrALTlem5VD  37345  2sb5ndVD  37370  2sb5ndALT  37392  ndisj2  37448  fourierdlem42  38124  fourierdlem42OLD  38125  2rmoswap  38750  ndmaovcom  38852  incistruhgr  39325  usgra2pth0  40177  eliunxp2  40623  pgrpgt2nabl  40659  islindeps  40754  lindslinindsimp1  40758  lindslinindsimp2  40764