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

Theorem bitr4i 244
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr4i.1  |-  ( ph  <->  ps )
bitr4i.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
bitr4i  |-  ( ph  <->  ch )

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2  |-  ( ph  <->  ps )
2 bitr4i.2 . . 3  |-  ( ch  <->  ps )
32bicomi 194 . 2  |-  ( ps  <->  ch )
41, 3bitri 241 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  3bitr2i  265  3bitr2ri  266  3bitr4i  269  3bitr4ri  270  imor  402  dfbi2  610  pm5.32  618  imdistan  671  imimorb  848  nbi2  863  pm5.6  879  mpbiran  885  mpbiran2  886  biluk  900  3anrev  947  nannan  1300  xorneg  1322  nic-ax  1447  nic-axALT  1448  19.43  1615  19.3v  1677  19.9vOLD  1710  equsalhwOLD  1861  nf3  1890  nf4  1891  equsalOLD  2000  sb6x  2108  sb5f  2128  sb3an  2144  sbequ8  2153  sb5  2175  sbhb  2182  pm11.07  2190  sbel2x  2201  eu2  2305  eu3  2306  eu5  2318  moanim  2336  2eu4  2363  2eu6  2365  cleqh  2532  cleqf  2595  necon3bii  2630  neor  2682  neorian  2685  r2alf  2732  r2exf  2733  r19.23t  2812  r19.26-3  2832  r19.26m  2833  r19.43  2855  rabid2  2877  isset  2952  ralv  2961  rexv  2962  reuv  2963  rmov  2964  rexcom4b  2969  ceqsex4v  2987  ceqsex8v  2989  ceqsrexv  3061  ralrab2  3092  rexrab2  3094  reu2  3114  reu3  3116  reueq  3123  2reuswap  3128  reuind  3129  2reu5lem3  3133  rmo2  3238  dfss2  3329  dfss3  3330  dfss3f  3332  ssabral  3406  rabss  3412  ssrabeq  3421  uniiunlem  3423  sspsstri  3441  npss  3449  uncom  3483  inass  3543  nsspssun  3566  dfss4  3567  dfun2  3568  dfin2  3569  indi  3579  indifdir  3589  difin2  3595  reupick3  3618  n0f  3628  eqv  3635  vss  3656  disj  3660  disj3  3664  undisj1  3671  undisj2  3672  inundif  3698  undif  3700  exsnrex  3840  euabsn2  3867  euabsn  3868  tppreqb  3931  pwpw0  3938  prssg  3945  ssunsn  3951  pwpr  4003  dfuni2  4009  unissb  4037  elint2  4049  ssint  4058  uniintab  4080  dfiin2g  4116  iunn0  4143  iunxun  4164  iunxiun  4165  iinpw  4171  disjor  4188  disjxiun  4201  dftr2  4296  dftr5  4297  dftr3  4298  dftr4  4299  vprc  4333  inuni  4354  snelpw  4402  sspwb  4405  pwssun  4481  dfid3  4491  dffr2  4539  dflim2  4629  orddif  4667  eusv2  4714  reusv2lem4  4719  reusv6OLD  4726  reusv7OLD  4727  rexxfr  4735  opthprc  4917  elxp3  4920  xpiundir  4925  elvv  4928  brinxp2  4931  relsn  4971  reliun  4987  inxp  4999  raliunxp  5006  cnvuni  5049  dm0rn0  5078  elrn  5102  ssdmres  5160  dfres2  5185  dfima2  5197  args  5224  dffr3  5228  cotr  5238  intasym  5241  asymref  5242  intirr  5244  cnv0  5267  xpnz  5284  xp11  5296  cnvresima  5351  resco  5366  rnco  5368  coiun  5371  coass  5380  cnvso  5403  dfiota2  5411  dffun2  5456  dffun6f  5460  dffun7  5471  dffun9  5473  funfn  5474  svrelfun  5506  dffn2  5584  dffn3  5590  fint  5614  dffn4  5651  dff1o4  5674  brprcneu  5713  eqfnfv3  5821  fnreseql  5832  fsn  5898  ftpg  5908  abrexco  5978  imaiun  5984  abexex  5995  dff13  5996  isocnv2  6043  mpt22eqb  6171  elovmpt2  6283  elxp6  6370  elxp7  6371  releldm2  6389  fnmpt2  6411  frxp  6448  dftpos4  6490  sorpss  6519  opiota  6527  tfrlem5  6633  tfrlem7  6636  ondif1  6737  oarec  6797  oeeu  6838  0er  6932  eroveu  6991  erovlem  6992  map0e  7043  elixpconst  7062  domen  7113  brsdom  7122  brdom2  7129  reuen1  7168  sbthlem10  7218  brsdom2  7223  xpf1o  7261  onfin2  7290  0sdom1dom  7298  modom  7301  unfi  7366  marypha2lem3  7434  dfsup2OLD  7440  wemapso2lem  7511  elom3  7595  dfom5  7597  trcl  7656  epfrs  7659  rankf  7712  scottexs  7803  scott0s  7804  cplem1  7805  karden  7811  hta  7813  pm54.43lem  7878  alephsuc2  7953  iscard3  7966  aceq0  7991  aceq3lem  7993  dfac3  7994  dfac5lem2  7997  dfac5  8001  dfac7  8004  dfac12a  8020  kmlem12  8033  kmlem14  8035  kmlem15  8036  infmap2  8090  ackbij2  8115  dfacfin7  8271  ituniiun  8294  zorng  8376  brdom7disj  8401  entri2  8425  alephreg  8449  fpwwe2lem12  8508  fpwwe2lem13  8509  pwfseqlem1  8525  grutsk  8689  axgroth4  8699  grothprim  8701  grothtsk  8702  elni2  8746  ltsopi  8757  genpass  8878  psslinpr  8900  ltexprlem4  8908  ltresr  9007  1re  9082  infm3  9959  elnnz  10284  dfz2  10291  2rexuz  10521  nnwos  10536  eluz2b1  10539  qexALT  10581  elxr  10708  dflt2  10733  xrsupss  10879  xrinfmss  10880  elixx1  10917  elioo2  10949  elioopnf  10990  elicopnf  10992  elfz1  11040  fznn0  11105  fznn  11107  injresinj  11192  nn0opthlem1  11553  faclbnd4lem1  11576  hashf  11617  hashfun  11692  hashf1  11698  fz1isolem  11702  f1oun2prg  11856  shftdm  11878  rediv  11928  imdiv  11935  rexanre  12142  caubnd  12154  climreu  12342  dvdslelem  12886  bitsval  12928  smueqlem  12994  algcvgblem  13060  isprm2  13079  isprm3  13080  isprm4  13081  pythagtriplem2  13183  elgz  13291  hashbc0  13365  0ram  13380  isstruct  13471  issect  13971  isfull2  14100  isfth2  14104  fucinv  14162  eldmcoa  14212  isdrs  14383  fpwipodrs  14582  submacs  14757  isnsg4  14975  isgim  15041  gaorb  15076  oppgid  15144  oppgsubm  15150  oppgcntz  15152  ispgp  15218  efgsdm  15354  efgcpbllema  15378  iscyg2  15484  isrng  15660  isirred2  15798  opprirred  15799  dfrhm2  15813  drngid2  15843  opprsubrg  15881  islmod  15946  lss1d  16031  islmhm  16095  islmim  16126  lbsextlem2  16223  lidlnz  16291  lidldvgen  16318  isnzr2  16326  isassa  16367  dfprm2  16766  isphl  16851  elocv  16887  iunocv  16900  isobs  16939  isbasis3g  17006  fctop  17060  cctop  17062  isclo2  17144  restsn  17226  lmbr  17314  ist0-3  17401  2ndcdisj  17511  1stccnp  17517  1stckgenlem  17577  txbas  17591  ptbasin  17601  tx2cn  17634  fbfinnfr  17865  fbasrn  17908  filuni  17909  ufinffr  17953  fin1aufil  17956  rnelfmlem  17976  flimrest  18007  alexsubALTlem3  18072  alexsubALTlem4  18073  tgphaus  18138  istlm  18206  iscusp2  18324  metuel2  18601  isngp2  18636  isnlm  18703  elcncf1di  18917  isphtpc  19011  phtpcer  19012  om1elbas  19049  isclm  19081  iscph  19125  iscau3  19223  minveclem3b  19321  elovolm  19363  ioombl1lem4  19447  dyaddisj  19480  vitali  19497  itg1climres  19598  itg2seq  19626  itg2monolem1  19634  itg2mono  19637  limcrcl  19753  lhop1  19890  itgsubst  19925  isuc1p  20055  ismon1p  20057  plydivex  20206  ellogdm  20522  1cubr  20674  atandm2  20709  birthdaylem3  20784  dmarea  20788  dchrelbas2  21013  dchrelbas4  21019  nb3grapr  21454  nb3grapr2  21455  cusgrarn  21460  usgrasscusgra  21484  3v3e3cycl2  21643  isgrpo2  21777  nmoubi  22265  nmobndseqi  22272  nmobndseqiOLD  22273  minvecolem1  22368  isch2  22718  hlimreui  22734  isch3  22736  ocsh  22777  dfch2  22901  spanuni  23038  nonbooli  23145  5oalem7  23154  adjsym  23328  elbdop2  23366  dmadjss  23382  nmopub  23403  nmfnleub  23420  nmop0h  23486  pjssposi  23667  pjordi  23668  cvbr2  23778  cvnbtwn2  23782  mdsl2i  23817  cvmdi  23819  elat2  23835  atom1d  23848  chirredi  23889  cdj3i  23936  or3di  23943  rabid2f  23959  mo5f  23964  2reuswap2  23967  rexunirn  23970  iuneq12daf  23999  iuneq12df  24000  iuninc  24003  disjorf  24013  rabfmpunirn  24057  mptfnf  24065  funcnv5mpt  24076  eliccelico  24132  elicoelioo  24133  isofld  24227  hasheuni  24467  pwsiga  24505  sigainb  24511  2ndmbfm  24603  probun  24669  ballotlem2  24738  ballotlemodife  24747  erdszelem9  24877  erdszelem10  24878  pconcon  24910  cvmliftiota  24980  nepss  25167  fzp1nel  25202  prodmo  25254  dfso2  25369  dfpo2  25370  dfres3  25374  elrn3  25378  elima4  25396  elpotr  25400  dfon2lem3  25404  dfon2lem5  25406  dfon2lem7  25408  dfon2lem8  25409  predreseq  25446  cbvsetlike  25448  dffr4  25449  preduz  25467  wfi  25474  frind  25510  soseq  25521  wfrlem5  25534  wfrlem8  25537  wfrlem11  25540  elwlim  25566  wzel  25567  frrlem5  25578  frrlem5c  25580  elno3  25602  nosgnn0  25605  nocvxminlem  25637  nofulllem5  25653  symdifass  25664  brtxp2  25718  brpprod3a  25723  eltrans  25728  dfon3  25729  dffix2  25742  dffun10  25751  elfuns  25752  brsingle  25754  brimg  25774  brsuccf  25778  funpartfun  25780  funpartfv  25782  axcontlem7  25901  cgrxfr  25981  segletr  26040  outsideoftr  26055  df3nandALT1  26138  rabiun2  26230  ismblfin  26237  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  itg2addnclem2  26247  islocfin  26367  neifg  26391  filnetlem4  26401  fdc  26440  nninfnub  26446  prdstotbnd  26494  isdrngo1  26563  ispridl  26635  ismaxidl  26641  prter1  26719  raldifsni  26725  rexrabdioph  26845  dford4  27091  islinds  27247  issdrg  27473  isdomn3  27491  pm11.52  27553  pm11.58  27557  pm13.192  27578  conss34  27612  bothtbothsame  27834  bothfbothsame  27835  aiffbtbat  27843  rmoanim  27924  2rmoswap  27929  frgra3v  28329  2spotdisj  28387  impexp3acom3r  28535  opelopab4  28575  uunT12p1  28849  uunT12p2  28850  uunT12p3  28851  uun2221  28862  uun2221p1  28863  uun2221p2  28864  undif3VD  28931  onfrALTlem5VD  28934  bnj252  29004  bnj253  29005  bnj255  29006  bnj345  29015  bnj133  29029  bnj976  29085  bnj1098  29091  bnj121  29178  bnj130  29182  bnj150  29184  bnj581  29216  bnj607  29224  bnj865  29231  bnj917  29242  bnj934  29243  bnj964  29251  bnj983  29259  bnj996  29263  bnj1021  29272  bnj1033  29275  bnj1047  29279  bnj1049  29280  bnj1090  29285  bnj1128  29296  bnj1175  29310  bnj1189  29315  bnj1204  29318  bnj1253  29323  bnj1312  29364  equsalNEW7  29424  sbequ8NEW7  29512  sb5NEW7  29535  sbhbwAUX7  29544  sbel2xNEW7  29551  sb6xNEW7  29566  sb5fNEW7  29571  sb3anNEW7  29577  sbhbOLD7  29697  islshp  29714  islshpat  29752  lcvbr2  29757  lcvnbtwn2  29762  cvrnbtwn3  30011  isatl  30034  ishlat1  30087  ishlat2  30088  cvrat4  30177  pmapglbx  30503  lhpexle3  30746  dib1dim  31900  diblsmopel  31906  lcfls1lem  32269
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