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

Theorem bitr4i 266
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 213 . 2 (𝜓𝜒)
41, 3bitri 263 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  3bitr2i  287  3bitr2ri  288  3bitr4i  291  3bitr4ri  292  imor  427  dfbi2  658  pm5.32  666  imdistan  721  bianass  838  imimorb  917  nbi2  932  pm5.6  949  mpbiran  955  mpbiran2  956  biluk  970  casesifp  1020  3anrev  1042  an3andi  1437  nancom  1442  nanbi  1446  xorneg  1468  cadan  1539  cadcomb  1543  nic-ax  1589  nic-axALT  1590  nf3  1703  19.43  1799  19.3v  1884  nf5  2102  nf6  2103  sb6x  2372  sb5f  2374  sb3an  2388  sbequ8ALT  2395  sb5  2418  sbhb  2426  sbnf2  2427  sbcom2  2433  eu1  2498  cleqh  2711  clelab  2735  necon3bii  2834  neor  2873  neorian  2876  r2allem  2921  r19.23t  3003  r19.26-3  3048  r19.26m  3049  r19.43  3074  rabid2  3096  eqvf  3177  isset  3180  ralv  3192  rexv  3193  reuv  3194  rmov  3195  rexcom4b  3200  ceqsex4v  3220  ceqsex8v  3222  ceqsrexv  3306  ralrab2  3339  rexrab2  3341  reu2  3361  reu3  3363  reueq  3371  2reuswap  3377  reuind  3378  2reu5lem3  3382  sbc3an  3461  rmo2  3492  dfss2  3557  dfss3  3558  dfss3f  3560  ssabral  3636  rabss  3642  ssrabeq  3651  uniiunlem  3653  sspsstri  3671  npss  3679  raldifb  3712  uncom  3719  inass  3785  symdifass  3815  nsspssun  3819  dfss4  3820  dfun2  3821  dfin2  3822  indi  3832  indifdir  3842  difin2  3849  reupick3  3871  eq0f  3884  neq0f  3885  n0fOLD  3887  rabn0  3912  csbab  3960  vss  3964  disj  3969  disj3  3973  undisj1  3981  undisj2  3982  inundif  3998  undif  4001  rabeqsn  4161  rabsssn  4162  exsnrex  4168  euabsn2  4204  euabsn  4205  raldifsni  4265  tppreqb  4277  pwpw0  4284  prssg  4290  ssunsn  4300  pwpr  4368  dfuni2  4374  unissb  4405  elint2  4417  ssint  4428  uniintab  4450  iuneq12df  4480  dfiin2g  4489  iunn0  4516  iunxun  4541  iunxiun  4544  iinpw  4550  disjor  4567  disjxiun  4579  disjxiunOLD  4580  dftr2  4682  dftr5  4683  dftr3  4684  dftr4  4685  vprc  4724  inuni  4753  eusv2  4791  reusv2lem4  4798  rexxfr  4814  snelpw  4840  sspwb  4844  opthneg  4876  pwssun  4944  dfid3  4954  dffr2  5003  opthprc  5089  elxp3  5092  xpiundir  5097  elvv  5100  brinxp2  5103  relsn  5146  reliun  5162  inxp  5176  raliunxp  5183  cnvuni  5231  dm0rn0  5263  elrn  5287  ssdmres  5340  dfres2  5372  dfima2  5387  args  5412  dffr3  5417  cotrg  5426  intasym  5430  asymref  5431  intirr  5433  cnv0OLD  5455  xpnz  5472  xp11  5488  xpimasn  5498  resco  5556  rnco  5558  coiun  5562  coass  5571  cnvso  5591  elsnxp  5594  elsnxpOLD  5595  dffr4  5613  wfi  5630  dflim2  5698  orddif  5737  dfiota2  5769  dffun2  5814  dffun6f  5818  dffun7  5830  dffun9  5832  funfn  5833  svrelfun  5875  mptfnf  5928  dffn2  5960  dffn3  5967  fint  5997  dffn4  6034  dff1o4  6058  brprcneu  6096  eqfnfv3  6221  fnreseql  6235  fsn  6308  ftpg  6328  abrexco  6406  imaiun  6407  dff13  6416  isof1oidb  6474  isof1oopb  6475  isocnv2  6481  mpt22eqb  6667  elovmpt2  6777  sorpss  6840  abexex  7042  elxp6  7091  elxp7  7092  releldm2  7109  opiota  7118  fnmpt2  7127  frxp  7174  cnvimadfsn  7191  mpt2xneldm  7225  dftpos4  7258  wfrlem8  7309  wfrfun  7312  dfrecs3  7356  tfrlem7  7366  ondif1  7468  oarec  7529  oeeu  7570  0er  7667  0erOLD  7668  eroveu  7729  erovlem  7730  map0e  7781  elixpconst  7802  domen  7854  brsdom  7864  brdom2  7871  reuen1  7911  sbthlem10  7964  brsdom2  7969  xpf1o  8007  onfin2  8037  0sdom1dom  8043  modom  8046  unfi  8112  marypha2lem3  8226  wemapsolem  8338  sucprcreg  8389  elom3  8428  dfom5  8430  trcl  8487  epfrs  8490  rankf  8540  scottexs  8633  scott0s  8634  cplem1  8635  karden  8641  hta  8643  pm54.43lem  8708  alephsuc2  8786  iscard3  8799  aceq0  8824  aceq3lem  8826  dfac3  8827  dfac5lem2  8830  dfac5  8834  dfac7  8837  dfac12a  8853  kmlem12  8866  kmlem14  8868  kmlem15  8869  infmap2  8923  ackbij2  8948  dfacfin7  9104  ituniiun  9127  zorng  9209  brdom7disj  9234  entri2  9259  alephreg  9283  fpwwe2lem12  9342  fpwwe2lem13  9343  pwfseqlem1  9359  grutsk  9523  axgroth4  9533  grothprim  9535  grothtsk  9536  elni2  9578  ltsopi  9589  genpass  9710  psslinpr  9732  ltexprlem4  9740  ltresr  9840  1re  9918  infm3  10861  elnnz  11264  dfz2  11272  2rexuz  11616  nnwos  11631  eluz2b1  11635  qexALT  11679  elxr  11826  dflt2  11857  xrsupss  12011  xrinfmss  12012  elixx1  12055  elioo2  12087  elioopnf  12138  elicopnf  12140  elfz1  12202  fznn  12278  fzp1nel  12293  fznn0  12301  preduz  12330  injresinj  12451  nn0opthlem1  12917  faclbnd4lem1  12942  hashfxnn0  12986  hashfOLD  12988  hashprdifel  13047  hashfun  13084  hashf1  13098  fz1isolem  13102  f1oun2prg  13512  brtrclfv  13591  shftdm  13659  rediv  13719  imdiv  13726  rexanre  13934  caubnd  13946  climreu  14135  prodmo  14505  dvdslelem  14869  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  bitsval  14984  smueqlem  15050  algcvgblem  15128  lcmfunsnlem2  15191  isprm2  15233  isprm3  15234  isprm4  15235  pythagtriplem2  15360  elgz  15473  hashbc0  15547  0ram  15562  isstruct  15705  issect  16236  isfull2  16394  isfth2  16398  fucinv  16456  eldmcoa  16538  isdrs  16757  fpwipodrs  16987  submacs  17188  isnsg4  17460  isgim  17527  gaorb  17563  oppgid  17609  oppgsubm  17615  oppgcntz  17617  ispgp  17830  efgsdm  17966  efgcpbllema  17990  iscyg2  18107  isring  18374  isirred2  18524  opprirred  18525  dfrhm2  18540  drngid2  18586  opprsubrg  18624  islmod  18690  lss1d  18784  islmhm  18848  islmim  18883  lbsextlem2  18980  lidlnz  19049  lidldvgen  19076  isnzr2  19084  isassa  19136  dfprm2  19661  isphl  19792  elocv  19831  iunocv  19844  isobs  19883  islinds  19967  1mavmul  20173  isbasis3g  20564  fctop  20618  cctop  20620  isclo2  20702  restsn  20784  lmbr  20872  ist0-3  20959  2ndcdisj  21069  1stccnp  21075  islocfin  21130  1stckgenlem  21166  txbas  21180  ptbasin  21190  tx2cn  21223  fbfinnfr  21455  fbasrn  21498  filuni  21499  ufinffr  21543  fin1aufil  21546  rnelfmlem  21566  flimrest  21597  alexsubALTlem3  21663  alexsubALTlem4  21664  tgphaus  21730  istlm  21798  iscusp2  21916  metuel2  22180  isngp2  22211  isnlm  22289  elcncf1di  22506  isphtpc  22601  phtpcer  22602  phtpcerOLD  22603  om1elbas  22640  isclm  22672  iscvsp  22736  iscph  22778  iscau3  22884  minveclem3b  23007  elovolm  23050  ioombl1lem4  23136  dyaddisj  23170  vitali  23188  itg1climres  23287  itg2seq  23315  itg2monolem1  23323  itg2mono  23326  limcrcl  23444  lhop1  23581  itgsubst  23616  mdegleb  23628  isuc1p  23704  ismon1p  23706  plydivex  23856  ellogdm  24185  1cubr  24369  atandm2  24404  birthdaylem3  24480  dmarea  24484  dchrelbas2  24762  dchrelbas4  24768  axcontlem7  25650  nb3grapr  25982  nb3grapr2  25983  cusgrarn  25988  usgrasscusgra  26011  3v3e3cycl2  26192  wwlkextwrd  26256  wwlkextinj  26258  isclwwlk  26296  erclwwlkref  26341  rusgranumwlkl1  26474  frgra3v  26529  2spotdisj  26588  numclwwlkovf2  26611  nmoubi  27011  nmobndseqi  27018  nmobndseqiALT  27019  minvecolem1  27114  isch2  27464  hlimreui  27480  isch3  27482  ocsh  27526  dfch2  27650  spanuni  27787  nonbooli  27894  5oalem7  27903  adjsym  28076  elbdop2  28114  dmadjss  28130  nmopub  28151  nmfnleub  28168  nmop0h  28234  pjssposi  28415  pjordi  28416  cvbr2  28526  cvnbtwn2  28530  mdsl2i  28565  cvmdi  28567  elat2  28583  atom1d  28596  chirredi  28637  cdj3i  28684  or3di  28691  moel  28707  mo5f  28708  2reuswap2  28712  rexunirn  28715  rabtru  28723  rabid2f  28724  iuneq12daf  28756  iuninc  28761  disjorf  28774  disjunsn  28789  rabfmpunirn  28833  aciunf1  28845  funcnv5mpt  28852  dfrp2  28922  eliccelico  28929  elicoelioo  28930  isomnd  29032  omndmul2  29043  isslmd  29086  hasheuni  29474  pwsiga  29520  sigainb  29526  issros  29565  2ndmbfm  29650  omssubaddlem  29688  omssubadd  29689  sitgaddlemb  29737  eulerpartlemgvv  29765  eulerpartlemn  29770  probun  29808  ballotlem2  29877  ballotlemodife  29886  bnj252  30022  bnj253  30023  bnj255  30024  bnj345  30033  bnj133  30047  bnj976  30102  bnj1098  30108  bnj121  30194  bnj130  30198  bnj150  30200  bnj581  30232  bnj607  30240  bnj865  30247  bnj917  30258  bnj934  30259  bnj964  30267  bnj983  30275  bnj996  30279  bnj1021  30288  bnj1033  30291  bnj1047  30295  bnj1049  30296  bnj1090  30301  bnj1128  30312  bnj1175  30326  bnj1189  30331  bnj1253  30339  bnj1312  30380  erdszelem9  30435  erdszelem10  30436  pconcon  30467  cvmliftiota  30537  elmthm  30727  nepss  30854  dfso2  30897  dfpo2  30898  dfres3  30902  elrn3  30906  elpotr  30930  dfon2lem5  30936  dfon2lem7  30938  dfon2lem8  30939  frind  30984  soseq  30995  elwlim  31013  elwlimOLD  31014  wzel  31015  wzelOLD  31016  frrlem5c  31030  elno3  31052  nosgnn0  31055  nosepon  31066  nocvxminlem  31089  nofulllem5  31105  brtxp2  31158  brpprod3a  31163  eltrans  31168  dfon3  31169  dffix2  31182  dffun10  31191  elfuns  31192  brsingle  31194  brimg  31214  funpartfun  31220  funpartfv  31222  cgrxfr  31332  segletr  31391  outsideoftr  31406  neifg  31536  filnetlem4  31546  df3nandALT1  31566  bj-consensusALT  31733  bj-biexal3  31885  bj-sb5  31956  bj-ralvw  32059  bj-rexvwv  32060  bj-rexcom4bv  32065  bj-rexcom4b  32066  bj-sbeq  32088  bj-inrab  32115  bj-xpima1snALT  32137  bj-dfmpt2a  32252  topdifinffinlem  32371  topdifinfeq  32374  relowlssretop  32387  relowlpssretop  32388  rdgeqoa  32394  wl-dfnan2  32475  wl-nannan  32477  rabiun  32552  phpreu  32563  fin2solem  32565  matunitlindflem2  32576  ptrest  32578  poimirlem25  32604  poimirlem27  32606  poimirlem30  32609  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem2  32632  fdc  32711  prdstotbnd  32763  isdrngo1  32925  ispridl  33003  ismaxidl  33009  impor  33050  selconj  33072  tradd  33077  scott0f  33147  prter1  33182  islshp  33284  islshpat  33322  lcvbr2  33327  lcvnbtwn2  33332  cvrnbtwn3  33581  isatl  33604  ishlat1  33657  ishlat2  33658  cvrat4  33747  pmapglbx  34073  lhpexle3  34316  dib1dim  35472  diblsmopel  35478  lcfls1lem  35841  rexrabdioph  36376  dford4  36614  issdrg  36786  isdomn3  36801  ifpdfor2  36824  ifpdfan2  36826  ifpdfor  36828  ifpdfan  36829  ifpdfbi  36837  ifpnot23b  36846  ifpnot23c  36848  ifpnot23d  36849  ifpim123g  36864  ifpbibib  36874  clss2lem  36937  imaiun1  36962  coiun1  36963  brfvrcld2  37003  iunrelexp0  37013  brtrclfv2  37038  snhesn  37100  dffrege76  37253  frege97  37274  frege98  37275  frege109  37286  frege110  37287  dffrege115  37292  frege131  37308  frege133  37310  ntrneineine1lem  37402  ntrneiel2  37404  ntrneiiso  37409  gneispace3  37451  pm11.52  37608  pm11.58  37612  pm13.192  37633  conss34OLD  37667  impexpdcom  37742  sbc3or  37759  opelopab4  37788  uunT12p1  38048  uunT12p2  38049  uunT12p3  38050  uun2221  38061  uun2221p1  38062  uun2221p2  38063  undif3VD  38140  onfrALTlem5VD  38143  ndisj2  38243  nssrex  38287  rabssf  38334  bothtbothsame  39715  bothfbothsame  39716  aiffbtbat  39724  rmoanim  39828  2rmoswap  39833  dfodd2  40087  dfeven5  40116  dfodd7  40117  1nevenALTV  40140  oddprmne2  40162  prinfzo0  40363  nb3grpr  40610  nb3grpr2  40611  upgr1wlkcompim  40851  wlkson  40864  wlkOnprop  40866  1wlksonproplem  40912  wwlknon  41053  wwlksnextinj  41105  elwspths2spth  41171  rusgrnumwwlkl1  41172  erclwwlksref  41241  frgr3v  41445  isrng  41666  isrnghm  41682  islindeps2  42066  isldepslvec2  42068  setrec1lem3  42235  aacllem  42356
  Copyright terms: Public domain W3C validator