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  2063  2mos  2222  2eu6  2228  abeq1i  2391  necon1bbii  2498  r19.41  2692  2ralor  2709  rexcom4a  2808  moeq  2941  euind  2952  2reuswap  2967  2reu5  2973  nfcdeq  2988  sbcid  3007  sbcco2  3014  sbc7  3018  sbcie2g  3024  eqsbc3  3030  sbcralt  3063  csbid  3088  cbvralcsf  3143  cbvrabcsf  3146  abss  3242  ssab  3243  difrab  3442  neq0  3465  vdif0  3514  ssunsn2  3773  sspr  3777  sstp  3778  prsspw  3785  uniintsn  3899  disjmoOLD  4008  brab1  4068  unopab  4095  axrep5  4136  axsep  4140  intexab  4169  wefrc  4387  ordelord  4414  uniuni  4527  reusv2lem4  4538  reusv2  4540  reuxfrd  4559  dfwe2  4573  orduniorsuc  4621  tfinds2  4654  elvvv  4749  eliunxp  4823  ralxp  4827  rexxp  4828  opelco  4853  reldm0  4896  resieq  4965  resiexg  4997  iss  4998  imai  5027  cnvsym  5057  intasym  5058  asymref  5059  codir  5063  poirr2  5067  rninxp  5117  dffun3  5266  funopg  5286  fin  5421  f1cnvcnv  5445  funimass4  5573  fnressn  5705  f1mpt  5785  resoprab  5940  mpt22eqb  5953  ov6g  5985  offval  6085  dfopab2  6174  dfoprab3s  6175  fmpt2x  6190  fparlem1  6218  fparlem2  6219  brtpos0  6241  dftpos3  6252  tpostpos  6254  tz7.48lem  6453  omeu  6583  ercnv  6681  ixp0  6849  xpcomco  6952  xpassen  6956  php  7045  findcard3  7100  ixpfi2  7154  marypha1lem  7186  dfsup2  7195  card2on  7268  infeq5i  7337  cnfcom3lem  7406  r1elss  7478  rankxplim  7549  scott0s  7558  aceq1  7744  dfac5lem1  7750  dfac5lem2  7751  kmlem3  7778  kmlem8  7783  kmlem16  7791  infpss  7843  cflem  7872  cf0  7877  alephval2  8194  rankcf  8399  r1tskina  8404  wfgru  8438  genpass  8633  psslinpr  8655  ltpsrpr  8731  infm3  9713  nnwos  10286  ioo0  10681  ico0  10702  ioc0  10703  icc0  10704  elfz2nn0  10821  sqeqori  11215  clim0  11980  dvdslelem  12573  divalglem6  12597  isprm2lem  12765  pceu  12899  prmreclem2  12964  isstruct  13158  xpscf  13468  acsfn2  13565  invsym2  13665  pospo  14107  efgrelexlemb  15059  gexex  15145  lssne0  15708  opsrtoslem1  16225  opsrtoslem2  16226  ntreq0  16814  ordtrest2lem  16933  ist0-3  17073  ist1-2  17075  ist1-3  17077  cmpfi  17135  2ndcctbss  17181  ptbasfi  17276  ptcnplem  17315  hausdiag  17339  hauseqlcld  17340  cnmptcom  17372  txflf  17701  tgphaus  17799  metrest  18070  iccpnfcnv  18442  bcth3  18753  volun  18902  dyadmax  18953  vitalilem2  18964  vitalilem3  18965  mbfimaopnlem  19010  itg2leub  19089  dvres2  19262  ellogdm  19986  reasinsin  20192  leibpilem2  20237  ftalem3  20312  dchreq  20497  lnon0  21376  spansncvi  22231  pjssmii  22260  nmlnopgt0i  22577  largei  22847  cvexchlem  22948  xfree  23024  addeq0  23043  ballotlemfp1  23050  ballotlem7  23094  eliccioo  23115  2reuswap2  23137  nmo  23144  cntnevol  23175  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  derang0  23700  iccllyscon  23781  cvmsss2  23805  axacprim  24053  dftr6  24107  dfpo2  24112  setinds2f  24135  elpotr  24137  tz6.26  24205  wfis2fg  24211  frins2fg  24247  tfrALTlem  24276  nobndlem1  24346  dfiota3  24462  funpartfv  24483  axcontlem2  24593  lineunray  24770  ellines  24775  hfninf  24816  dfoprab4pop  25037  issubcata  25846  inixp  26399  heibor1lem  26533  4rexfrabdioph  26879  dford4  27122  islindf4  27308  f1omvdco3  27392  psgnunilem5  27417  isdomn3  27523  fgraphopab  27529  2rmoswap  27962  ndmaovcom  28065  frgra3v  28180  opelopab4  28317  2sb5nd  28326  un2122  28565  uunT12p4  28578  onfrALTlem5VD  28661  2sb5ndVD  28686  2sb5ndALT  28709  bnj446  28742  bnj563  28772  bnj110  28890  bnj153  28912  bnj557  28933  bnj864  28954  bnj865  28955  bnj849  28957  bnj929  28968  bnj1110  29012  islshpat  29207  lkr0f  29284  lshpsmreu  29299  cvrnbtwn4  29469  ishlat2  29543  islvol5  29768  tendoeq2  30963  dibelval3  31337  mapdpglem3  31865  hdmapglem7a  32120
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