Theorem bitr3i 251

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 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  485  orordi  527  orordir  528  anandi  817  anandir  818  trunantru  1404  falnanfal  1407  cadanOLD  1437  had0  1448  nic-axALT  1484  sbied  2100  sbidm  2110  sb6a  2157  sbelx  2170  sbco4  2181  mo  2294  2eu6  2363  abeq1i  2541  necon1bbii  2653  r19.41  2862  2ralor  2880  rexcom4a  2983  moeq  3124  2reuswap  3150  2reu5  3156  nfcdeq  3172  sbcid  3191  sbcco2  3198  sbc7  3202  sbcie2g  3208  eqsbc3  3214  sbcralt  3255  cbvralcsf  3307  cbvrabcsf  3310  abss  3409  ssab  3410  difrab  3612  neq0  3635  sbccsb  3689  vdif0  3726  difrab0eq  3727  ssunsn2  4020  sspr  4024  sstp  4025  prsspw  4033  uniintsn  4153  disjmoOLD  4265  brab1  4325  unopab  4355  axrep5  4396  axsep  4400  intexab  4438  reusv2lem4  4484  reusv2  4486  reuxfrd  4505  wefrc  4701  ordelord  4728  elvvv  4885  eliunxp  4964  ralxp  4968  rexxp  4969  opelco  4998  reldm0  5044  resieq  5108  iss  5142  imai  5169  cnvsym  5200  intasym  5201  asymref  5202  codir  5206  poirr2  5210  xpdifid  5254  rninxp  5265  dffun3  5417  funopg  5438  fin  5579  f1cnvcnv  5602  funimass4  5730  fnressn  5881  resoprab  6175  mpt22eqb  6188  elrnmpt2res  6193  ov6g  6217  offval  6316  uniuni  6374  dfwe2  6382  orduniorsuc  6430  tfinds2  6463  resiexg  6503  dfopab2  6617  dfoprab3s  6618  fmpt2x  6629  fparlem1  6661  fparlem2  6662  brtpos0  6741  dftpos3  6752  tpostpos  6754  tz7.48lem  6882  omeu  7012  ercnv  7110  ixp0  7284  xpcomco  7389  xpassen  7393  php  7483  findcard3  7543  ixpfi2  7597  dfsup2  7680  card2on  7757  infeq5i  7830  cnfcom3lem  7924  cnfcom3lemOLD  7932  r1elss  8001  rankxplim  8074  scott0s  8083  aceq1  8275  dfac5lem1  8281  dfac5lem2  8282  kmlem3  8309  kmlem8  8314  kmlem16  8322  cflem  8403  cf0  8408  alephval2  8724  rankcf  8932  r1tskina  8937  wfgru  8971  genpass  9166  psslinpr  9188  ltpsrpr  9264  infm3  10277  nnwos  10910  ioo0  11313  ico0  11334  ioc0  11335  icc0  11336  elfz2nn0  11467  elfzmlbp  11478  sqeqori  11962  hashgt12el  12157  hashgt12el2  12158  cshwidxmod  12424  clim0  12968  dvdslelem  13560  divalglem6  13585  isprm2lem  13753  pceu  13896  prmreclem2  13961  cshwshash  14114  isstruct  14167  xpscf  14487  acsfn2  14584  invsym2  14684  pospo  15126  f1omvdco3  15935  psgnunilem5  15980  efgrelexlemb  16227  gexex  16315  lssne0  16954  opsrtoslem1  17497  opsrtoslem2  17498  islindf4  18109  mdetunilem8  18267  ntreq0  18523  ordtrest2lem  18649  ist0-3  18791  ist1-2  18793  ist1-3  18795  cmpfi  18853  2ndcctbss  18901  ptbasfi  18996  ptcnplem  19036  hausdiag  19060  hauseqlcld  19061  cnmptcom  19093  txflf  19421  tgphaus  19529  metrest  19941  iccpnfcnv  20358  bcth3  20684  volun  20868  dyadmax  20920  vitalilem2  20931  vitalilem3  20932  mbfimaopnlem  20975  itg2leub  21054  dvres2  21229  ellogdm  21969  reasinsin  22176  leibpilem2  22221  ftalem3  22297  dchreq  22482  axcontlem2  23034  lnon0  24021  spansncvi  24878  pjssmii  24907  nmlnopgt0i  25224  largei  25494  cvexchlem  25595  xfree  25671  nmo  25693  2reuswap2  25696  fpwrelmapffslem  25857  addeq0  25860  eliccioo  25929  omndmul2  25999  ordtrest2NEWlem  26206  ordtconlem1  26208  xrge0iifcnv  26217  xrge0iifiso  26219  xrge0iifhom  26221  cntnevol  26496  eulerpartlemgh  26609  ballotlemfp1  26722  ballotlem7  26766  signswch  26810  derang0  26905  iccllyscon  26987  cvmsss2  27011  axacprim  27205  dftr6  27407  dfpo2  27412  opelco3  27436  elima4  27437  setinds2f  27439  elpotr  27441  tz6.26  27513  wfis2fg  27519  frins2fg  27555  wzel  27608  nobndlem1  27680  elfuns  27793  dfiota3  27801  imagesset  27831  lineunray  28025  ellines  28030  hfninf  28071  finixpnum  28258  fin2so  28260  tan2h  28268  ovoliunnfl  28277  voliunnfl  28279  ftc1anc  28319  inixp  28466  heibor1lem  28552  sbccom2lem  28777  csbcom2fi  28782  tsna1  28799  4rexfrabdioph  28981  dford4  29223  isdomn3  29417  fgraphopab  29423  2rmoswap  29854  ndmaovcom  29957  rabasiun  30076  wlk0  30138  usgra2pth0  30148  rusgranumwlklem0  30412  frgra3v  30440  4cycl2vnunb  30455  vdn0frgrav2  30462  vdgn0frgrav2  30463  usg2spot2nb  30504  eliunxp2  30566  pgrpgt2nabel  30600  islindeps  30696  lindslinindsimp1  30700  lindslinindsimp2  30706  opelopab4  30961  2sb5nd  30970  un2122  31225  uunT12p4  31238  onfrALTlem5VD  31323  2sb5ndVD  31348  2sb5ndALT  31370  bnj446  31407  bnj563  31437  bnj110  31553  bnj153  31575  bnj557  31596  bnj864  31617  bnj865  31618  bnj849  31620  bnj929  31631  bnj1110  31675  bj-axrep5  31933  bj-axsep  31934  bj-rexcom4a  31986  bj-snglc  32045  islshpat  32235  lkr0f  32312  lshpsmreu  32327  cvrnbtwn4  32497  ishlat2  32571  islvol5  32796  tendoeq2  33991  dibelval3  34365  mapdpglem3  34893  hdmapglem7a  35148