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

Theorem bitr3i 242
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 193 . 2  |-  ( ph  <->  ps )
3 bitr3i.2 . 2  |-  ( ps  <->  ch )
42, 3bitri 240 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  3bitrri  263  3bitr3i  266  3bitr3ri  267  xchnxbi  299  ianor  474  orordi  516  orordir  517  anandi  801  anandir  802  trunantru  1344  falnanfal  1347  cadan  1382  had0  1393  nic-axALT  1429  sbelx  2076  2mos  2235  2eu6  2241  abeq1i  2404  necon1bbii  2511  r19.41  2705  2ralor  2722  rexcom4a  2821  moeq  2954  euind  2965  2reuswap  2980  2reu5  2986  nfcdeq  3001  sbcid  3020  sbcco2  3027  sbc7  3031  sbcie2g  3037  eqsbc3  3043  sbcralt  3076  csbid  3101  cbvralcsf  3156  cbvrabcsf  3159  abss  3255  ssab  3256  difrab  3455  neq0  3478  vdif0  3527  ssunsn2  3789  sspr  3793  sstp  3794  prsspw  3801  uniintsn  3915  disjmoOLD  4024  brab1  4084  unopab  4111  axrep5  4152  axsep  4156  intexab  4185  wefrc  4403  ordelord  4430  uniuni  4543  reusv2lem4  4554  reusv2  4556  reuxfrd  4575  dfwe2  4589  orduniorsuc  4637  tfinds2  4670  elvvv  4765  eliunxp  4839  ralxp  4843  rexxp  4844  opelco  4869  reldm0  4912  resieq  4981  resiexg  5013  iss  5014  imai  5043  cnvsym  5073  intasym  5074  asymref  5075  codir  5079  poirr2  5083  rninxp  5133  dffun3  5282  funopg  5302  fin  5437  f1cnvcnv  5461  funimass4  5589  fnressn  5721  f1mpt  5801  resoprab  5956  mpt22eqb  5969  ov6g  6001  offval  6101  dfopab2  6190  dfoprab3s  6191  fmpt2x  6206  fparlem1  6234  fparlem2  6235  brtpos0  6257  dftpos3  6268  tpostpos  6270  tz7.48lem  6469  omeu  6599  ercnv  6697  ixp0  6865  xpcomco  6968  xpassen  6972  php  7061  findcard3  7116  ixpfi2  7170  marypha1lem  7202  dfsup2  7211  card2on  7284  infeq5i  7353  cnfcom3lem  7422  r1elss  7494  rankxplim  7565  scott0s  7574  aceq1  7760  dfac5lem1  7766  dfac5lem2  7767  kmlem3  7794  kmlem8  7799  kmlem16  7807  infpss  7859  cflem  7888  cf0  7893  alephval2  8210  rankcf  8415  r1tskina  8420  wfgru  8454  genpass  8649  psslinpr  8671  ltpsrpr  8747  infm3  9729  nnwos  10302  ioo0  10697  ico0  10718  ioc0  10719  icc0  10720  elfz2nn0  10837  sqeqori  11231  clim0  11996  dvdslelem  12589  divalglem6  12613  isprm2lem  12781  pceu  12915  prmreclem2  12980  isstruct  13174  xpscf  13484  acsfn2  13581  invsym2  13681  pospo  14123  efgrelexlemb  15075  gexex  15161  lssne0  15724  opsrtoslem1  16241  opsrtoslem2  16242  ntreq0  16830  ordtrest2lem  16949  ist0-3  17089  ist1-2  17091  ist1-3  17093  cmpfi  17151  2ndcctbss  17197  ptbasfi  17292  ptcnplem  17331  hausdiag  17355  hauseqlcld  17356  cnmptcom  17388  txflf  17717  tgphaus  17815  metrest  18086  iccpnfcnv  18458  bcth3  18769  volun  18918  dyadmax  18969  vitalilem2  18980  vitalilem3  18981  mbfimaopnlem  19026  itg2leub  19105  dvres2  19278  ellogdm  20002  reasinsin  20208  leibpilem2  20253  ftalem3  20328  dchreq  20513  lnon0  21392  spansncvi  22247  pjssmii  22276  nmlnopgt0i  22593  largei  22863  cvexchlem  22964  xfree  23040  addeq0  23059  ballotlemfp1  23066  ballotlem7  23110  eliccioo  23131  2reuswap2  23153  nmo  23160  cntnevol  23191  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  derang0  23715  iccllyscon  23796  cvmsss2  23820  axacprim  24068  dftr6  24178  dfpo2  24183  setinds2f  24206  elpotr  24208  tz6.26  24276  wfis2fg  24282  frins2fg  24318  tfrALTlem  24347  nobndlem1  24417  dfiota3  24533  axcontlem2  24665  lineunray  24842  ellines  24847  hfninf  24888  ovoliunnfl  25001  dfoprab4pop  25140  issubcata  25949  inixp  26502  heibor1lem  26636  4rexfrabdioph  26982  dford4  27225  islindf4  27411  f1omvdco3  27495  psgnunilem5  27520  isdomn3  27626  fgraphopab  27632  2rmoswap  28065  ndmaovcom  28173  hashgt12el  28218  hashgt12el2  28219  frgra3v  28426  4cycl2vnunb  28439  opelopab4  28616  2sb5nd  28625  un2122  28879  uunT12p4  28892  onfrALTlem5VD  28977  2sb5ndVD  29002  2sb5ndALT  29025  bnj446  29058  bnj563  29088  bnj110  29206  bnj153  29228  bnj557  29249  bnj864  29270  bnj865  29271  bnj849  29273  bnj929  29284  bnj1110  29328  sbelxNEW7  29585  islshpat  29829  lkr0f  29906  lshpsmreu  29921  cvrnbtwn4  30091  ishlat2  30165  islvol5  30390  tendoeq2  31585  dibelval3  31959  mapdpglem3  32487  hdmapglem7a  32742
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 177
  Copyright terms: Public domain W3C validator