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  826  anandir  827  trunantru  1421  falnanfal  1424  cadanOLD  1444  had0  1455  nic-axALT  1491  sbied  2125  sbidm  2132  sb6a  2177  sbelx  2190  sbco4  2201  mo  2322  2eu6  2393  2eu6OLD  2394  bm1.1  2450  abeq1iOLD  2597  cbvab  2608  necon1bbiiOLD  2732  nabbi  2800  r19.41  3013  2ralor  3031  rexcom4a  3134  moeq  3279  2reuswap  3306  2reu5  3312  nfcdeq  3328  sbcid  3348  sbcco2  3355  sbc7  3359  sbcie2g  3365  eqsbc3  3371  sbcralt  3412  cbvralcsf  3467  cbvrabcsf  3470  abss  3569  ssab  3570  difrab  3772  neq0  3795  sbccsb  3849  vdif0  3886  difrab0eq  3887  ssunsn2  4186  sspr  4190  sstp  4191  prsspw  4199  uniintsn  4319  rabasiun  4329  disjmoOLD  4432  brab1  4492  unopab  4522  axrep5  4563  axsep  4567  intexab  4605  reusv2lem4  4651  reusv2  4653  reuxfrd  4672  wefrc  4873  ordelord  4900  elvvv  5059  eliunxp  5140  ralxp  5144  rexxp  5145  opelco  5174  reldm0  5220  resieq  5284  iss  5321  imai  5349  cnvsym  5381  intasym  5382  asymref  5383  codir  5387  poirr2  5391  xpdifid  5435  rninxp  5446  dffun3  5599  funopg  5620  fin  5765  f1cnvcnv  5789  funimass4  5918  fnressn  6073  resoprab  6382  mpt22eqb  6395  elrnmpt2res  6400  ov6g  6424  offval  6531  uniuni  6593  dfwe2  6601  orduniorsuc  6649  tfinds2  6682  resiexg  6720  dfopab2  6838  dfoprab3s  6839  fmpt2x  6850  fparlem1  6883  fparlem2  6884  brtpos0  6962  dftpos3  6973  tpostpos  6975  tz7.48lem  7106  omeu  7234  ercnv  7332  ixp0  7502  xpcomco  7607  xpassen  7611  php  7701  findcard3  7763  ixpfi2  7818  dfsup2  7902  card2on  7980  infeq5i  8053  cnfcom3lem  8147  cnfcom3lemOLD  8155  r1elss  8224  rankxplim  8297  scott0s  8306  aceq1  8498  dfac5lem1  8504  dfac5lem2  8505  kmlem3  8532  kmlem8  8537  kmlem16  8545  cflem  8626  cf0  8631  alephval2  8947  rankcf  9155  r1tskina  9160  wfgru  9194  genpass  9387  psslinpr  9409  ltpsrpr  9486  infm3  10502  nnwos  11149  ioo0  11554  ico0  11575  ioc0  11576  icc0  11577  elfz2nn0  11768  elfzmlbp  11783  sqeqori  12248  hashgt12el  12446  hashgt12el2  12447  cshwidxmod  12737  clim0  13292  dvdslelem  13889  divalglem6  13915  isprm2lem  14083  pceu  14229  prmreclem2  14294  cshwshash  14447  isstruct  14500  xpscf  14821  acsfn2  14918  invsym2  15018  pospo  15460  f1omvdco3  16280  psgnunilem5  16325  efgrelexlemb  16574  gexex  16662  srgrmhm  16989  lssne0  17397  opsrtoslem1  17947  opsrtoslem2  17948  islindf4  18668  mdetunilem8  18916  cpmatmcllem  19014  pmatcollpw2lem  19073  ntreq0  19372  ordtrest2lem  19498  ist0-3  19640  ist1-2  19642  ist1-3  19644  cmpfi  19702  2ndcctbss  19750  ptbasfi  19845  ptcnplem  19885  hausdiag  19909  hauseqlcld  19910  cnmptcom  19942  txflf  20270  tgphaus  20378  metrest  20790  iccpnfcnv  21207  bcth3  21533  volun  21718  dyadmax  21770  vitalilem2  21781  vitalilem3  21782  mbfimaopnlem  21825  itg2leub  21904  dvres2  22079  ellogdm  22776  reasinsin  22983  leibpilem2  23028  ftalem3  23104  dchreq  23289  legso  23740  axcontlem2  23972  wlk0  24465  rusgranumwlklem0  24652  frgra3v  24706  4cycl2vnunb  24721  vdn0frgrav2  24728  vdgn0frgrav2  24729  usg2spot2nb  24770  lnon0  25417  spansncvi  26274  pjssmii  26303  nmlnopgt0i  26620  largei  26890  cvexchlem  26991  xfree  27067  nmo  27088  2reuswap2  27091  fpwrelmapffslem  27255  addeq0  27258  eliccioo  27323  omndmul2  27392  ordtrest2NEWlem  27568  ordtconlem1  27570  xrge0iifcnv  27579  xrge0iifiso  27581  xrge0iifhom  27583  qtophaus  27665  cntnevol  27867  eulerpartlemgh  27985  ballotlemfp1  28098  ballotlem7  28142  signswch  28186  derang0  28281  iccllyscon  28363  cvmsss2  28387  axacprim  28582  dftr6  28784  dfpo2  28789  opelco3  28813  elima4  28814  setinds2f  28816  elpotr  28818  tz6.26  28890  wfis2fg  28896  frins2fg  28932  wzel  28985  nobndlem1  29057  elfuns  29170  dfiota3  29178  imagesset  29208  lineunray  29402  ellines  29407  hfninf  29448  finixpnum  29643  fin2so  29645  tan2h  29652  ovoliunnfl  29661  voliunnfl  29663  ftc1anc  29703  inixp  29850  heibor1lem  29936  sbccom2lem  30161  csbcom2fi  30166  tsna1  30183  4rexfrabdioph  30363  dford4  30603  isdomn3  30797  fgraphopab  30803  ellimcabssub0  31187  fourierdlem42  31477  2rmoswap  31684  ndmaovcom  31785  usgra2pth0  31850  eliunxp2  32019  pgrpgt2nabl  32056  islindeps  32153  lindslinindsimp1  32157  lindslinindsimp2  32163  opelopab4  32422  2sb5nd  32431  un2122  32685  uunT12p4  32698  onfrALTlem5VD  32783  2sb5ndVD  32808  2sb5ndALT  32830  bnj446  32867  bnj563  32897  bnj110  33013  bnj153  33035  bnj557  33056  bnj864  33077  bnj865  33078  bnj849  33080  bnj929  33091  bnj1110  33135  bj-axrep5  33477  bj-axsep  33478  bj-rexcom4a  33545  bj-snglc  33626  islshpat  33832  lkr0f  33909  lshpsmreu  33924  cvrnbtwn4  34094  ishlat2  34168  islvol5  34393  tendoeq2  35588  dibelval3  35962  mapdpglem3  36490  hdmapglem7a  36745