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

Theorem bitr4i 243
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 193 . 2  |-  ( ps  <->  ch )
41, 3bitri 240 1  |-  ( ph  <->  ch )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  3bitr2i  264  3bitr2ri  265  3bitr4i  268  3bitr4ri  269  imor  401  dfbi2  609  pm5.32  617  imdistan  670  imimorb  847  nbi2  862  pm5.6  878  mpbiran  884  mpbiran2  885  biluk  899  3anrev  945  nannan  1291  xorneg  1304  nic-ax  1428  nic-axALT  1429  19.43  1594  19.9v  1665  equsalhw  1732  nf3  1801  nf4  1802  equsal  1902  sb6x  1971  sb5f  1982  sb3an  2012  sbequ8  2021  sb5  2041  sbhb  2048  sbel2x  2066  eu2  2170  eu3  2171  eu5  2183  moanim  2201  2eu4  2228  2eu6  2230  cleqh  2382  cleqf  2445  necon3bii  2480  neor  2532  neorian  2535  r2alf  2580  r2exf  2581  r19.23t  2659  r19.26-3  2679  r19.26m  2680  r19.43  2697  rabid2  2719  isset  2794  ralv  2803  rexv  2804  reuv  2805  rmov  2806  rexcom4b  2811  ceqsex4v  2829  ceqsex8v  2831  ceqsrexv  2903  ralrab2  2933  rexrab2  2935  reu2  2955  reu3  2957  reueq  2964  2reuswap  2969  reuind  2970  2reu5lem3  2974  rmo2  3078  dfss2  3171  dfss3  3172  dfss3f  3174  ssabral  3246  rabss  3252  uniiunlem  3262  sspsstri  3280  npss  3288  uncom  3321  inass  3381  nsspssun  3404  dfss4  3405  dfun2  3406  dfin2  3407  indi  3417  indifdir  3427  difin2  3432  reupick3  3455  n0f  3465  eqv  3472  vss  3493  disj  3497  disj3  3501  undisj1  3508  undisj2  3509  inundif  3534  undif  3536  euabsn2  3700  euabsn  3701  pwpw0  3765  prssg  3772  ssunsn  3776  pwpr  3825  dfuni2  3831  unissb  3859  elint2  3871  ssint  3880  uniintab  3902  dfiin2g  3938  iunn0  3964  iunxun  3985  iunxiun  3986  iinpw  3992  disjor  4009  disjxiun  4022  dftr2  4117  dftr5  4118  dftr3  4119  dftr4  4120  vprc  4154  inuni  4175  snelpw  4223  sspwb  4225  pwssun  4301  dfid3  4312  dffr2  4360  dflim2  4450  orddif  4488  eusv2  4535  reusv2lem4  4540  reusv6OLD  4547  reusv7OLD  4548  rexxfr  4556  opthprc  4738  elxp3  4741  xpiundir  4746  elvv  4750  brinxp2  4753  relsn  4792  reliun  4808  inxp  4820  raliunxp  4827  cnvuni  4868  dm0rn0  4897  elrn  4921  ssdmres  4979  dfres2  5004  dfima2  5016  args  5043  dffr3  5047  cotr  5057  intasym  5060  asymref  5061  intirr  5063  cnv0  5086  xpnz  5101  xp11  5113  cnvresima  5164  resco  5179  rnco  5181  coiun  5184  coass  5193  cnvso  5216  dfiota2  5222  dffun2  5267  dffun6f  5271  dffun7  5282  dffun9  5284  funfn  5285  svrelfun  5315  dffn2  5392  dffn3  5398  fint  5422  dffn4  5459  dff1o4  5482  brprcneu  5520  eqfnfv3  5626  fnreseql  5637  fsn  5698  abrexco  5768  imaiun  5773  abexex  5784  dff13  5785  isocnv2  5830  mpt22eqb  5955  elovmpt2  6066  elxp6  6153  elxp7  6154  releldm2  6172  fnmpt2  6194  frxp  6227  dftpos4  6255  sorpss  6284  opiota  6292  tfrlem5  6398  tfrlem7  6401  ondif1  6502  oarec  6562  oeeu  6603  0er  6697  eroveu  6755  erovlem  6756  map0e  6807  elixpconst  6826  domen  6877  brsdom  6886  brdom2  6893  reuen1  6932  sbthlem10  6982  brsdom2  6987  xpf1o  7025  onfin2  7054  0sdom1dom  7062  modom  7065  unfi  7126  marypha2lem3  7192  dfsup2OLD  7198  wemapso2lem  7267  elom3  7351  dfom5  7353  trcl  7412  epfrs  7415  rankf  7468  scottexs  7559  scott0s  7560  cplem1  7561  karden  7567  hta  7569  pm54.43lem  7634  alephsuc2  7709  iscard3  7722  aceq0  7747  aceq3lem  7749  dfac3  7750  dfac5lem2  7753  dfac5  7757  dfac7  7760  dfac12a  7776  kmlem12  7789  kmlem14  7791  kmlem15  7792  infmap2  7846  ackbij2  7871  ominf4  7940  dfacfin7  8027  ituniiun  8050  zorng  8133  brdom7disj  8158  entri2  8182  alephreg  8206  fpwwe2lem12  8265  fpwwe2lem13  8266  pwfseqlem1  8282  grutsk  8446  axgroth4  8456  grothprim  8458  grothtsk  8459  elni2  8503  ltsopi  8514  genpass  8635  psslinpr  8657  ltexprlem4  8665  ltresr  8764  1re  8839  infm3  9715  elnnz  10036  dfz2  10043  2rexuz  10273  nnwos  10288  eluz2b1  10291  qexALT  10333  elxr  10460  dflt2  10484  xrsupss  10629  xrinfmss  10630  elixx1  10667  elioo2  10699  elioopnf  10739  elicopnf  10741  elfz1  10789  fznn0  10853  fznn  10854  nn0opthlem1  11285  faclbnd4lem1  11308  hashf  11346  hashfun  11391  hashf1  11397  fz1isolem  11401  shftdm  11568  rediv  11618  imdiv  11625  rexanre  11832  caubnd  11844  climreu  12032  dvdslelem  12575  bitsval  12617  smueqlem  12683  algcvgblem  12749  isprm2  12768  isprm3  12769  isprm4  12770  pythagtriplem2  12872  elgz  12980  hashbc0  13054  0ram  13069  isstruct  13160  issect  13658  isssc  13699  isfull2  13787  isfth2  13791  fucinv  13849  eldmcoa  13899  isdrs  14070  fpwipodrs  14269  submacs  14444  isnsg4  14662  isgim  14728  gaorb  14763  oppgid  14831  oppgsubm  14837  oppgcntz  14839  ispgp  14905  efgsdm  15041  efgcpbllema  15065  iscyg2  15171  isrng  15347  isirred2  15485  opprirred  15486  dfrhm2  15500  drngid2  15530  opprsubrg  15568  islmod  15633  lss1d  15722  islmhm  15786  islmim  15817  lbsextlem2  15914  lidlnz  15982  lidldvgen  16009  isnzr2  16017  isassa  16058  dfprm2  16449  isphl  16534  elocv  16570  iunocv  16583  isobs  16622  isbasis3g  16689  fctop  16743  cctop  16745  isclo2  16827  restsn  16903  lmbr  16990  ist0-3  17075  2ndcdisj  17184  1stccnp  17190  1stckgenlem  17250  txbas  17264  ptbasin  17274  tx2cn  17306  fbfinnfr  17538  fbasrn  17581  filuni  17582  ufinffr  17626  fin1aufil  17629  rnelfmlem  17649  flimrest  17680  alexsubALTlem3  17745  alexsubALTlem4  17746  tgphaus  17801  istlm  17869  isngp2  18121  isnlm  18188  elcncf1di  18401  isphtpc  18494  phtpcer  18495  om1elbas  18532  isclm  18564  iscph  18608  iscau3  18706  minveclem3b  18794  elovolm  18836  ioombl1lem4  18920  dyaddisj  18953  vitali  18970  itg1climres  19071  itg2seq  19099  itg2monolem1  19107  itg2mono  19110  limcrcl  19226  lhop1  19363  itgsubst  19398  isuc1p  19528  ismon1p  19530  plydivex  19679  ellogdm  19988  1cubr  20140  atandm2  20175  birthdaylem3  20250  dmarea  20254  dchrelbas2  20478  dchrelbas4  20484  isgrpo2  20866  nmoubi  21352  nmobndseqi  21359  nmobndseqiOLD  21360  minvecolem1  21455  isch2  21805  hlimreui  21821  isch3  21823  ocsh  21864  dfch2  21988  spanuni  22125  nonbooli  22232  5oalem7  22241  adjsym  22415  elbdop2  22453  dmadjss  22469  nmopub  22490  nmfnleub  22507  nmop0h  22573  pjssposi  22754  pjordi  22755  cvbr2  22865  cvnbtwn2  22869  mdsl2i  22904  cvmdi  22906  elat2  22922  atom1d  22935  chirredi  22976  cdj3i  23023  ballotlem2  23049  ballotlemodife  23058  or3di  23125  rabid2f  23137  2reuswap2  23139  rexunirn  23142  mo5f  23145  iuneq12daf  23156  iuneq12df  23157  iuninc  23160  disjex  23178  disjexc  23179  rabfmpunirn  23219  mptfnf  23228  funcnv5mpt  23238  eliccelico  23272  elicoelioo  23273  disjorf  23358  hasheuni  23455  pwsiga  23493  sigainb  23499  2ndmbfm  23568  isibfm  23595  probun  23624  erdszelem9  23732  erdszelem10  23733  pconcon  23764  cvmliftiota  23834  nepss  24074  dfso2  24113  dfpo2  24114  dfres3  24118  elrn3  24122  elpotr  24139  dfon2lem3  24143  dfon2lem5  24145  dfon2lem7  24147  dfon2lem8  24148  predreseq  24181  cbvsetlike  24183  dffr4  24184  preduz  24202  wfi  24209  frind  24245  soseq  24256  wfrlem5  24262  wfrlem8  24265  wfrlem11  24268  frrlem5  24287  frrlem5c  24289  elno3  24311  nosgnn0  24314  nocvxminlem  24346  nofulllem5  24362  symdifass  24373  brtxp2  24423  brpprod3a  24428  eltrans  24433  dfon3  24434  elfuns  24456  brsingle  24458  brsuccf  24482  funpartfun  24483  axcontlem7  24600  cgrxfr  24680  segletr  24739  outsideoftr  24754  df3nandALT1  24837  rabiun2  24929  itg2addnclem2  24934  itg2addnc  24935  dfdir2  25302  ishomc  25800  isconcl7a  26116  isibcg  26202  cnvresimaOLD  26237  islocfin  26307  neifg  26331  filnetlem4  26341  fdc  26466  nninfnub  26472  prdstotbnd  26529  isdrngo1  26598  ispridl  26670  ismaxidl  26676  prter1  26758  raldifsni  26764  rexrabdioph  26886  dford4  27133  islinds  27290  issdrg  27516  isdomn3  27534  pm11.52  27596  pm11.58  27600  pm13.192  27621  conss34  27656  stoweidlem52  27812  rmoanim  27968  2rmoswap  27973  f1oun2prg  28087  mpt2xopynvov0g  28091  frgra3v  28191  impexp3acom3r  28333  opelopab4  28373  uunT12p1  28646  uunT12p2  28647  uunT12p3  28648  uun2221  28659  uun2221p1  28660  uun2221p2  28661  undif3VD  28731  onfrALTlem5VD  28734  bnj252  28801  bnj253  28802  bnj255  28803  bnj345  28812  bnj133  28826  bnj976  28882  bnj1098  28888  bnj121  28975  bnj130  28979  bnj150  28981  bnj581  29013  bnj607  29021  bnj865  29028  bnj917  29039  bnj934  29040  bnj964  29048  bnj983  29056  bnj996  29060  bnj1021  29069  bnj1033  29072  bnj1047  29076  bnj1049  29077  bnj1090  29082  bnj1128  29093  bnj1175  29107  bnj1189  29112  bnj1204  29115  bnj1253  29120  bnj1312  29161  anandii  29180  islshp  29242  islshpat  29280  lcvbr2  29285  lcvnbtwn2  29290  cvrnbtwn3  29539  isatl  29562  ishlat1  29615  ishlat2  29616  cvrat4  29705  pmapglbx  30031  lhpexle3  30274  dib1dim  31428  diblsmopel  31434  lcfls1lem  31797
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