Theorem bitr3i 243

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

Syntax hints:   <-> wb 177

This theorem is referenced by:  3bitrri  264  3bitr3i  267  3bitr3ri  268  xchnxbi  300  ianor  475  orordi  517  orordir  518  anandi  802  anandir  803  trunantru  1360  falnanfal  1363  cadan  1398  had0  1409  nic-axALT  1445  sbelx  2174  2eu6  2339  abeq1i  2512  necon1bbii  2619  r19.41  2820  2ralor  2837  rexcom4a  2936  moeq  3070  2reuswap  3096  2reu5  3102  nfcdeq  3118  sbcid  3137  sbcco2  3144  sbc7  3148  sbcie2g  3154  eqsbc3  3160  sbcralt  3193  cbvralcsf  3271  cbvrabcsf  3274  abss  3372  ssab  3373  difrab  3575  neq0  3598  vdif0  3647  difrab0eq  3648  ssunsn2  3918  sspr  3922  sstp  3923  prsspw  3931  uniintsn  4047  disjmoOLD  4157  brab1  4217  unopab  4244  axrep5  4285  axsep  4289  intexab  4318  wefrc  4536  ordelord  4563  uniuni  4675  reusv2lem4  4686  reusv2  4688  reuxfrd  4707  dfwe2  4721  orduniorsuc  4769  tfinds2  4802  elvvv  4896  eliunxp  4971  ralxp  4975  rexxp  4976  opelco  5003  reldm0  5046  resieq  5115  resiexg  5147  iss  5148  imai  5177  cnvsym  5207  intasym  5208  asymref  5209  codir  5213  poirr2  5217  rninxp  5269  dffun3  5424  funopg  5444  fin  5582  f1cnvcnv  5606  funimass4  5736  fnressn  5877  resoprab  6125  mpt22eqb  6138  ov6g  6170  offval  6271  dfopab2  6360  dfoprab3s  6361  fmpt2x  6376  fparlem1  6405  fparlem2  6406  brtpos0  6445  dftpos3  6456  tpostpos  6458  tz7.48lem  6657  omeu  6787  ercnv  6885  ixp0  7054  xpcomco  7157  xpassen  7161  php  7250  findcard3  7309  ixpfi2  7363  dfsup2  7405  card2on  7478  infeq5i  7547  cnfcom3lem  7616  r1elss  7688  rankxplim  7759  scott0s  7768  aceq1  7954  dfac5lem1  7960  dfac5lem2  7961  kmlem3  7988  kmlem8  7993  kmlem16  8001  cflem  8082  cf0  8087  alephval2  8403  rankcf  8608  r1tskina  8613  wfgru  8647  genpass  8842  psslinpr  8864  ltpsrpr  8940  infm3  9923  nnwos  10500  ioo0  10897  ico0  10918  ioc0  10919  icc0  10920  elfz2nn0  11038  sqeqori  11448  hashgt12el  11637  hashgt12el2  11638  clim0  12255  dvdslelem  12849  divalglem6  12873  isprm2lem  13041  pceu  13175  prmreclem2  13240  isstruct  13434  xpscf  13746  acsfn2  13843  invsym2  13943  pospo  14385  efgrelexlemb  15337  gexex  15423  lssne0  15982  opsrtoslem1  16499  opsrtoslem2  16500  ntreq0  17096  ordtrest2lem  17221  ist0-3  17363  ist1-2  17365  ist1-3  17367  cmpfi  17425  2ndcctbss  17471  ptbasfi  17566  ptcnplem  17606  hausdiag  17630  hauseqlcld  17631  cnmptcom  17663  txflf  17991  tgphaus  18099  metrest  18507  iccpnfcnv  18922  bcth3  19237  volun  19392  dyadmax  19443  vitalilem2  19454  vitalilem3  19455  mbfimaopnlem  19500  itg2leub  19579  dvres2  19752  ellogdm  20483  reasinsin  20689  leibpilem2  20734  ftalem3  20810  dchreq  20995  lnon0  22252  spansncvi  23107  pjssmii  23136  nmlnopgt0i  23453  largei  23723  cvexchlem  23824  xfree  23900  nmo  23926  2reuswap2  23928  addeq0  24067  eliccioo  24130  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  cntnevol  24535  ballotlemfp1  24702  ballotlem7  24746  derang0  24808  iccllyscon  24890  cvmsss2  24914  axacprim  25109  dftr6  25321  dfpo2  25326  setinds2f  25349  elpotr  25351  tz6.26  25419  wfis2fg  25425  frins2fg  25461  tfrALTlem  25490  nobndlem1  25560  dfiota3  25676  axcontlem2  25808  lineunray  25985  ellines  25990  hfninf  26031  ovoliunnfl  26147  voliunnfl  26149  inixp  26320  heibor1lem  26408  4rexfrabdioph  26748  dford4  26990  islindf4  27176  f1omvdco3  27260  psgnunilem5  27285  isdomn3  27391  fgraphopab  27397  2rmoswap  27829  ndmaovcom  27936  elfzmlbp  27978  usgra2pth0  28042  frgra3v  28106  4cycl2vnunb  28121  vdn0frgrav2  28128  vdgn0frgrav2  28129  usg2spot2nb  28168  opelopab4  28349  2sb5nd  28358  un2122  28611  uunT12p4  28624  onfrALTlem5VD  28706  2sb5ndVD  28731  2sb5ndALT  28754  bnj446  28787  bnj563  28817  bnj110  28935  bnj153  28957  bnj557  28978  bnj864  28999  bnj865  29000  bnj849  29002  bnj929  29013  bnj1110  29057  sbelxNEW7  29314  islshpat  29500  lkr0f  29577  lshpsmreu  29592  cvrnbtwn4  29762  ishlat2  29836  islvol5  30061  tendoeq2  31256  dibelval3  31630  mapdpglem3  32158  hdmapglem7a  32413

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

This theorem depends on definitions:  df-bi 178