MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bitr3i Structured version   Unicode version

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
StepHypRef Expression
1 bitr3i.1 . . 3  |-  ( ps  <->  ph )
21bicomi 194 . 2  |-  ( ph  <->  ps )
3 bitr3i.2 . 2  |-  ( ps  <->  ch )
42, 3bitri 241 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
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  1363  falnanfal  1366  cadan  1401  had0  1412  nic-axALT  1448  sbied  2150  sbelx  2201  2eu6  2366  abeq1i  2544  necon1bbii  2656  r19.41  2860  2ralor  2877  rexcom4a  2976  moeq  3110  2reuswap  3136  2reu5  3142  nfcdeq  3158  sbcid  3177  sbcco2  3184  sbc7  3188  sbcie2g  3194  eqsbc3  3200  sbcralt  3233  cbvralcsf  3311  cbvrabcsf  3314  abss  3412  ssab  3413  difrab  3615  neq0  3638  vdif0  3687  difrab0eq  3688  ssunsn2  3958  sspr  3962  sstp  3963  prsspw  3971  uniintsn  4087  disjmoOLD  4197  brab1  4257  unopab  4284  axrep5  4325  axsep  4329  intexab  4358  wefrc  4576  ordelord  4603  uniuni  4716  reusv2lem4  4727  reusv2  4729  reuxfrd  4748  dfwe2  4762  orduniorsuc  4810  tfinds2  4843  elvvv  4937  eliunxp  5012  ralxp  5016  rexxp  5017  opelco  5044  reldm0  5087  resieq  5156  resiexg  5188  iss  5189  imai  5218  cnvsym  5248  intasym  5249  asymref  5250  codir  5254  poirr2  5258  rninxp  5310  dffun3  5465  funopg  5485  fin  5623  f1cnvcnv  5647  funimass4  5777  fnressn  5918  resoprab  6166  mpt22eqb  6179  ov6g  6211  offval  6312  dfopab2  6401  dfoprab3s  6402  fmpt2x  6417  fparlem1  6446  fparlem2  6447  brtpos0  6486  dftpos3  6497  tpostpos  6499  tz7.48lem  6698  omeu  6828  ercnv  6926  ixp0  7095  xpcomco  7198  xpassen  7202  php  7291  findcard3  7350  ixpfi2  7405  dfsup2  7447  card2on  7522  infeq5i  7591  cnfcom3lem  7660  r1elss  7732  rankxplim  7803  scott0s  7812  aceq1  7998  dfac5lem1  8004  dfac5lem2  8005  kmlem3  8032  kmlem8  8037  kmlem16  8045  cflem  8126  cf0  8131  alephval2  8447  rankcf  8652  r1tskina  8657  wfgru  8691  genpass  8886  psslinpr  8908  ltpsrpr  8984  infm3  9967  nnwos  10544  ioo0  10941  ico0  10962  ioc0  10963  icc0  10964  elfz2nn0  11082  sqeqori  11493  hashgt12el  11682  hashgt12el2  11683  clim0  12300  dvdslelem  12894  divalglem6  12918  isprm2lem  13086  pceu  13220  prmreclem2  13285  isstruct  13479  xpscf  13791  acsfn2  13888  invsym2  13988  pospo  14430  efgrelexlemb  15382  gexex  15468  lssne0  16027  opsrtoslem1  16544  opsrtoslem2  16545  ntreq0  17141  ordtrest2lem  17267  ist0-3  17409  ist1-2  17411  ist1-3  17413  cmpfi  17471  2ndcctbss  17518  ptbasfi  17613  ptcnplem  17653  hausdiag  17677  hauseqlcld  17678  cnmptcom  17710  txflf  18038  tgphaus  18146  metrest  18554  iccpnfcnv  18969  bcth3  19284  volun  19439  dyadmax  19490  vitalilem2  19501  vitalilem3  19502  mbfimaopnlem  19547  itg2leub  19626  dvres2  19799  ellogdm  20530  reasinsin  20736  leibpilem2  20781  ftalem3  20857  dchreq  21042  lnon0  22299  spansncvi  23154  pjssmii  23183  nmlnopgt0i  23500  largei  23770  cvexchlem  23871  xfree  23947  nmo  23973  2reuswap2  23975  addeq0  24114  eliccioo  24177  xrge0iifcnv  24319  xrge0iifiso  24321  xrge0iifhom  24323  cntnevol  24582  ballotlemfp1  24749  ballotlem7  24793  derang0  24855  iccllyscon  24937  cvmsss2  24961  axacprim  25156  dftr6  25373  dfpo2  25378  opelco3  25403  elima4  25404  setinds2f  25406  elpotr  25408  tz6.26  25480  wfis2fg  25486  frins2fg  25522  wzel  25575  nobndlem1  25647  elfuns  25760  dfiota3  25768  imagesset  25798  axcontlem2  25904  lineunray  26081  ellines  26086  hfninf  26127  ovoliunnfl  26248  voliunnfl  26250  ftc1anc  26288  inixp  26430  heibor1lem  26518  4rexfrabdioph  26858  dford4  27100  islindf4  27285  f1omvdco3  27369  psgnunilem5  27394  isdomn3  27500  fgraphopab  27506  2rmoswap  27938  ndmaovcom  28045  elfzmlbp  28107  cshwssize  28290  usgra2pth0  28312  frgra3v  28392  4cycl2vnunb  28407  vdn0frgrav2  28414  vdgn0frgrav2  28415  usg2spot2nb  28454  opelopab4  28638  2sb5nd  28647  un2122  28902  uunT12p4  28915  onfrALTlem5VD  28997  2sb5ndVD  29022  2sb5ndALT  29044  bnj446  29081  bnj563  29111  bnj110  29229  bnj153  29251  bnj557  29272  bnj864  29293  bnj865  29294  bnj849  29296  bnj929  29307  bnj1110  29351  sbelxNEW7  29613  ax7w14lemAUX7  29669  islshpat  29815  lkr0f  29892  lshpsmreu  29907  cvrnbtwn4  30077  ishlat2  30151  islvol5  30376  tendoeq2  31571  dibelval3  31945  mapdpglem3  32473  hdmapglem7a  32728
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
  Copyright terms: Public domain W3C validator