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

Theorem bitr4i 267
Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
Hypotheses
Ref Expression
bitr4i.1 (𝜑𝜓)
bitr4i.2 (𝜒𝜓)
Assertion
Ref Expression
bitr4i (𝜑𝜒)

Proof of Theorem bitr4i
StepHypRef Expression
1 bitr4i.1 . 2 (𝜑𝜓)
2 bitr4i.2 . . 3 (𝜒𝜓)
32bicomi 214 . 2 (𝜓𝜒)
41, 3bitri 264 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  3bitr2i  288  3bitr2ri  289  3bitr4i  292  3bitr4ri  293  imor  426  dfbi2  660  pm5.32  668  imdistan  724  bianass  874  imimorb  954  nbi2  969  pm5.6  986  mpbiran  988  mpbiran2  989  biluk  1009  casesifp  1061  3ancoma  1081  3ancomb  1083  3anrev  1088  an3andi  1591  nancom  1596  nanbi  1600  xorneg  1622  cadan  1694  cadcomb  1698  nic-ax  1744  nic-axALT  1745  nf3  1858  nfnbi  1929  19.43  1960  19.3v  2064  sb5  2271  nf5  2277  nf6  2278  sb6x  2529  sb5f  2531  sb3an  2545  sbequ8ALT  2552  sbhb  2586  sbnf2  2587  sbcom2  2591  eu1  2657  cleqh  2871  clelab  2895  necon3bii  2993  neor  3032  neorian  3035  r2allem  3084  r19.23t  3167  r19.26-3  3212  r19.26m  3213  r19.43  3239  rabid2  3265  rabid2f  3266  eqvf  3352  isset  3355  ralv  3367  rexv  3368  reuv  3369  rmov  3370  rexcom4b  3375  ceqsex4v  3395  ceqsex8v  3397  ceqsrexv  3483  rabtru  3509  ralrab2  3521  rexrab2  3523  reu2  3543  reu3  3545  reueq  3553  2reuswap  3559  reuind  3560  2reu5lem3  3564  sbc3an  3642  rmo2  3672  dfss2  3737  dfss3  3738  dfss3f  3741  ssabral  3819  rabss  3825  ssrabeq  3836  uniiunlem  3838  sspsstri  3856  npss  3864  dfdif3  3868  raldifb  3898  uncom  3905  inass  3969  symdifass  3999  nsspssun  4003  dfss4  4004  dfun2  4005  dfin2  4006  indi  4019  indifdir  4029  difin2  4035  reupick3  4057  eq0f  4070  neq0f  4071  rabn0  4101  csbab  4149  vss  4153  disj  4157  disj3  4161  undisj1  4169  undisj2  4170  inundif  4185  undif  4188  rabeqsn  4349  rabsssn  4350  exsnrex  4356  euabsn2  4393  euabsn  4394  raldifsni  4458  tppreqb  4468  pwpw0  4476  prssg  4482  ssunsn  4491  preqsn  4524  pwpr  4565  dfuni2  4573  unissb  4602  elint2  4615  ssint  4624  uniintab  4646  iuneq12df  4675  dfiin2g  4684  iunn0  4711  iunxun  4736  iunxiun  4739  iinpw  4748  disjor  4765  disjxiun  4780  dftr2  4885  dftr5  4886  dftr3  4887  dftr4  4888  vprc  4926  inuni  4953  eusv2  4992  reusv2lem4  4999  rexxfr  5015  snelpw  5040  sspwb  5044  opthneg  5076  pwssun  5152  dfid3  5157  dffr2  5213  opthprc  5306  elxp3  5308  xpiundir  5313  elvv  5316  brinxp2  5319  relsnOLD  5365  reliun  5377  inxp  5392  raliunxp  5399  cnvuni  5446  dm0rn0  5479  elrn  5503  dfres3  5538  ssdmres  5560  dfres2  5593  dfima2  5608  args  5633  dffr3  5638  cotrg  5647  intasym  5651  asymref  5652  intirr  5654  cnv0OLD  5676  xpnz  5693  xp11  5709  xpimasn  5719  resco  5782  rnco  5784  coiun  5788  coass  5797  cnvso  5817  elsnxp  5820  dffr4  5838  wfi  5855  dflim2  5923  orddif  5962  dfiota2  5994  dffun2  6040  dffun6f  6044  dffun7  6057  dffun9  6059  funfn  6060  svrelfun  6100  mptfnf  6154  dffn2  6186  dffn3  6193  fint  6223  dffn4  6261  dff1o4  6285  brprcneu  6324  eqfnfv3  6455  fnreseql  6469  fsn  6543  ftpg  6564  abrexco  6643  imaiun  6644  dff13  6653  isof1oidb  6715  isof1oopb  6716  isocnv2  6722  mpt22eqb  6914  elovmpt2  7024  sorpss  7087  abexex  7296  elxp6  7347  elxp7  7348  releldm2  7365  opiota  7376  fnmpt2  7386  frxp  7436  cnvimadfsn  7453  mpt2xneldm  7488  dftpos4  7521  wfrlem8  7573  wfrfun  7576  dfrecs3  7620  tfrlem7  7630  ondif1  7733  oarec  7794  oeeu  7835  0er  7931  eroveu  7993  erovlem  7994  map0eOLD  8046  elixpconst  8068  domen  8120  brsdom  8130  brdom2  8137  reuen1  8176  sbthlem10  8233  brsdom2  8238  xpf1o  8276  onfin2  8306  0sdom1dom  8312  modom  8315  unfi  8381  marypha2lem3  8497  wemapsolem  8609  sucprcreg  8660  elom3  8707  dfom5  8709  trcl  8766  epfrs  8769  rankf  8819  scottexs  8912  scott0s  8913  cplem1  8914  karden  8920  hta  8922  pm54.43lem  9023  alephsuc2  9101  iscard3  9114  aceq0  9139  aceq3lem  9141  dfac3  9142  dfac5lem2  9145  dfac5  9149  dfac7  9154  dfac12a  9170  kmlem12  9183  kmlem14  9185  kmlem15  9186  infmap2  9240  ackbij2  9265  dfacfin7  9421  ituniiun  9444  zorng  9526  brdom7disj  9553  entri2  9580  alephreg  9604  fpwwe2lem12  9663  fpwwe2lem13  9664  pwfseqlem1  9680  grutsk  9844  axgroth4  9854  grothprim  9856  grothtsk  9857  elni2  9899  ltsopi  9910  genpass  10031  psslinpr  10053  ltexprlem4  10061  ltresr  10161  1re  10239  infm3  11182  elnnz  11587  dfz2  11595  2rexuz  11941  nnwos  11957  eluz2b1  11961  qexALT  12005  elxr  12154  dflt2  12185  xrsupss  12343  xrinfmss  12344  elixx1  12388  elioo2  12420  elioopnf  12472  elicopnf  12474  elfz1  12537  fznn  12614  fzp1nel  12630  fznn0  12638  preduz  12668  prinfzo0  12714  injresinj  12796  nn0opthlem1  13262  faclbnd4lem1  13287  hashfxnn0  13331  hashfOLD  13333  hashprdifel  13391  hashfun  13429  hashf1  13446  fz1isolem  13450  f1oun2prg  13874  brtrclfv  13954  shftdm  14022  rediv  14082  imdiv  14089  rexanre  14297  caubnd  14309  climreu  14498  prodmo  14877  dvdslelem  15245  3dvdsdec  15268  3dvdsdecOLD  15269  3dvds2dec  15270  3dvds2decOLD  15271  bitsval  15360  smueqlem  15426  algcvgblem  15504  lcmfunsnlem2  15567  isprm2  15608  isprm3  15609  isprm4  15610  pythagtriplem2  15735  elgz  15848  hashbc0  15922  0ram  15937  isstruct  16083  issect  16626  isfull2  16784  isfth2  16788  fucinv  16846  eldmcoa  16928  isdrs  17148  fpwipodrs  17378  submacs  17579  isnsg4  17851  isgim  17918  gaorb  17953  oppgid  17999  oppgsubm  18005  oppgcntz  18007  ispgp  18220  efgsdm  18356  efgcpbllema  18380  iscyg2  18497  isring  18765  isirred2  18915  opprirred  18916  dfrhm2  18933  drngid2  18979  opprsubrg  19017  islmod  19083  lss1d  19182  islmhm  19246  islmim  19281  lbsextlem2  19380  lidlnz  19449  lidldvgen  19476  isnzr2  19484  isassa  19536  dfprm2  20063  isphl  20196  elocv  20235  iunocv  20248  isobs  20287  islinds  20371  1mavmul  20578  isbasis3g  20980  fctop  21035  cctop  21037  isclo2  21119  restsn  21201  lmbr  21289  ist0-3  21376  2ndcdisj  21486  1stccnp  21492  islocfin  21547  1stckgenlem  21583  txbas  21597  ptbasin  21607  tx2cn  21640  fbfinnfr  21871  fbasrn  21914  filuni  21915  ufinffr  21959  fin1aufil  21962  rnelfmlem  21982  flimrest  22013  alexsubALTlem3  22079  alexsubALTlem4  22080  tgphaus  22146  istlm  22214  iscusp2  22332  metuel2  22596  isngp2  22627  isnlm  22705  elcncf1di  22924  isphtpc  23019  phtpcer  23020  om1elbas  23057  isclm  23089  iscvsp  23153  iscph  23195  iscau3  23301  minveclem3b  23424  elovolm  23469  ioombl1lem4  23555  dyaddisj  23590  vitali  23607  itg1climres  23707  itg2seq  23735  itg2monolem1  23743  itg2mono  23746  limcrcl  23864  lhop1  24003  itgsubst  24038  mdegleb  24050  isuc1p  24126  ismon1p  24128  plydivex  24278  ellogdm  24612  1cubr  24796  atandm2  24831  birthdaylem3  24907  dmarea  24911  dchrelbas2  25189  dchrelbas4  25195  axcontlem7  26077  nb3grpr  26513  nb3grpr2  26514  upgrwlkcompim  26780  wlkson  26793  wlkonprop  26795  wksonproplem  26842  ispth  26860  wwlknon  26994  wwlknonOLD  26996  wwlksnextinj  27048  wspthsnwspthsnon  27065  elwspths2spth  27120  rusgrnumwwlkl1  27121  clwwlkccatlem  27143  erclwwlkref  27174  frgr3v  27461  nmoubi  27968  nmobndseqi  27975  nmobndseqiALT  27976  minvecolem1  28071  isch2  28421  hlimreui  28437  isch3  28439  ocsh  28483  dfch2  28607  spanuni  28744  nonbooli  28851  5oalem7  28860  adjsym  29033  elbdop2  29071  dmadjss  29087  nmopub  29108  nmfnleub  29125  nmop0h  29191  pjssposi  29372  pjordi  29373  cvbr2  29483  cvnbtwn2  29487  mdsl2i  29522  cvmdi  29524  elat2  29540  atom1d  29553  chirredi  29594  cdj3i  29641  or3di  29648  moel  29664  mo5f  29665  2reuswap2  29668  rexunirn  29671  difrab2  29678  difininv  29693  iuneq12daf  29712  iuninc  29718  disjorf  29731  disjunsn  29746  rabfmpunirn  29794  aciunf1  29804  funcnv5mpt  29810  dfrp2  29873  eliccelico  29880  elicoelioo  29881  isomnd  30042  omndmul2  30053  isslmd  30096  hasheuni  30488  pwsiga  30534  sigainb  30540  issros  30579  2ndmbfm  30664  omssubaddlem  30702  omssubadd  30703  sitgaddlemb  30751  eulerpartlemgvv  30779  eulerpartlemn  30784  probun  30822  ballotlem2  30891  ballotlemodife  30900  bnj252  31110  bnj253  31111  bnj255  31112  bnj345  31121  bnj133  31134  bnj976  31187  bnj1098  31193  bnj121  31279  bnj130  31283  bnj150  31285  bnj581  31317  bnj607  31325  bnj865  31332  bnj917  31343  bnj934  31344  bnj964  31352  bnj983  31360  bnj996  31364  bnj1021  31373  bnj1033  31376  bnj1047  31380  bnj1049  31381  bnj1090  31386  bnj1128  31397  bnj1175  31411  bnj1189  31416  bnj1253  31424  bnj1312  31465  erdszelem9  31520  erdszelem10  31521  pconnconn  31552  cvmliftiota  31622  elmthm  31812  nepss  31938  dfso2  31983  dfpo2  31984  elrn3  31991  imaindm  32019  elpotr  32023  dfon2lem5  32029  dfon2lem7  32031  dfon2lem8  32032  frpoind  32078  frind  32081  soseq  32092  elwlim  32106  wzel  32107  frrlem5c  32124  elno3  32146  nosgnn0  32149  nosepon  32156  nocvxminlem  32231  scutcut  32250  scutbday  32251  dmscut  32256  scutf  32257  sltrec  32262  brtxp2  32326  brpprod3a  32331  eltrans  32336  dfon3  32337  dffix2  32350  dffun10  32359  elfuns  32360  brsingle  32362  brimg  32382  funpartfun  32388  funpartfv  32390  cgrxfr  32500  segletr  32559  outsideoftr  32574  neifg  32704  filnetlem4  32714  df3nandALT1  32734  bj-consensusALT  32901  bj-biexal3  33036  bj-sb5  33105  bj-ralvw  33195  bj-rexvwv  33196  bj-rexcom4bv  33201  bj-rexcom4b  33202  bj-sbeq  33226  bj-inrab  33256  bj-xpima1snALT  33276  bj-dfmpt2a  33403  topdifinffinlem  33532  topdifinfeq  33535  relowlssretop  33548  relowlpssretop  33549  rdgeqoa  33555  wl-dfnan2  33633  wl-nannan  33635  rabiun  33715  phpreu  33726  fin2solem  33728  matunitlindflem2  33739  ptrest  33741  poimirlem25  33767  poimirlem27  33769  poimirlem30  33772  ismblfin  33783  ovoliunnfl  33784  voliunnfl  33786  volsupnfl  33787  itg2addnclem2  33794  fdc  33873  prdstotbnd  33925  isdrngo1  34087  ispridl  34165  ismaxidl  34171  impor  34212  selconj  34234  tradd  34239  scott0f  34309  biancom  34339  inxpss3  34427  idinxpssinxp2  34432  idinxpssinxp3  34433  dfrel5  34456  ineleq  34461  moantr  34469  dfxrn2  34480  inxpxrn  34495  rnxrnres  34499  1cossres  34526  cocossss  34533  cossssid4  34562  cossssid5  34563  cosscnvssid5  34570  cossid  34572  dfssr2  34591  cnvrefrelcoss2  34625  cosselcnvrefrels2  34626  prter1  34687  islshp  34788  islshpat  34826  lcvbr2  34831  lcvnbtwn2  34836  cvrnbtwn3  35085  isatl  35108  ishlat1  35161  ishlat2  35162  cvrat4  35251  pmapglbx  35577  lhpexle3  35820  dib1dim  36975  diblsmopel  36981  lcfls1lem  37344  rexrabdioph  37884  dford4  38122  issdrg  38293  isdomn3  38308  ifpdfor2  38331  ifpdfan2  38333  ifpdfor  38335  ifpdfan  38336  ifpdfbi  38344  ifpnot23b  38353  ifpnot23c  38355  ifpnot23d  38356  ifpim123g  38371  ifpbibib  38381  clss2lem  38444  imaiun1  38469  coiun1  38470  brfvrcld2  38510  iunrelexp0  38520  brtrclfv2  38545  snhesn  38606  dffrege76  38759  frege97  38780  frege98  38781  frege109  38792  frege110  38793  dffrege115  38798  frege131  38814  frege133  38816  ntrneineine1lem  38908  ntrneiel2  38910  ntrneiiso  38915  gneispace3  38957  pm11.52  39112  pm11.58  39116  pm13.192  39137  conss34OLD  39172  impexpdcom  39247  sbc3or  39264  opelopab4  39293  uunT12p1  39553  uunT12p2  39554  uunT12p3  39555  uun2221  39566  uun2221p1  39567  uun2221p2  39568  undif3VD  39641  ndisj2  39740  nssrex  39782  rabssf  39824  bothtbothsame  41587  bothfbothsame  41588  aiffbtbat  41596  rmoanim  41700  2rmoswap  41705  dfodd2  42074  dfeven5  42103  dfodd7  42104  1nevenALTV  42127  oddprmne2  42149  isrng  42401  isrnghm  42417  islindeps2  42797  isldepslvec2  42799  setrec1lem3  42961  aacllem  43075
  Copyright terms: Public domain W3C validator