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

Theorem bitr4i 281
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 227 . 2 (𝜓𝜒)
41, 3bitri 278 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 209
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 210
This theorem is referenced by:  3bitr2i  302  3bitr2ri  303  3bitr4i  306  3bitr4ri  307  biluk  390  biancomi  466  dfbi2  478  imdistan  571  pm5.32  577  bianass  641  mpbiran  708  biadaniALT  820  imor  850  imimorb  948  pm5.6  999  nbi2  1013  casesifp  1074  3ancoma  1095  3ancomb  1096  3anrev  1098  an3andi  1479  nanimn  1485  nannan  1488  nanbi  1491  xorcom  1505  xorneg  1515  xorbi12i  1516  norcom  1523  noran  1527  norasslem1  1531  norassOLD  1535  trunortru  1587  trunorfal  1589  cadan  1611  cadcomb  1615  nic-ax  1675  nic-axALT  1676  nf3  1788  nfnbi  1856  19.43  1883  19.3vOLD  1989  equsv  2009  sb3an  2086  sbrimvlem  2098  sbcom2  2165  sb5OLD  2277  nf5  2286  nf6  2287  sb6x  2476  2sb5rf  2485  2sb6rf  2486  sb4b  2488  sb4bOLD  2489  sb5f  2516  sbequ8  2520  sbhb  2540  sb5ALT2  2562  sb5fALT  2579  eu6lem  2633  eu1  2671  cleqh  2913  clelab  2933  cleqf  2983  necon3bii  3039  neor  3078  neorian  3081  r19.26-3  3139  r19.26m  3140  r2allem  3165  r19.23t  3272  r19.43  3304  rexcom  3308  rabid2  3334  rabid2f  3335  eqv  3449  eqvf  3450  isset  3453  ralv  3466  rexv  3467  reuv  3468  rmov  3469  rexcom4b  3471  ceqsex4v  3494  ceqsex8v  3496  ceqsrexv  3597  ralrab2  3638  rexrab2  3641  reu2  3664  reu3  3666  reueq  3676  2reuswap  3685  2reuswap2  3686  reuind  3692  2reu5lem3  3696  2rmoswap  3700  sbc3an  3785  rmo2  3816  rmoanim  3823  rmoanimALT  3824  dfss2  3901  dfss2OLD  3902  dfss3  3903  dfss3f  3906  ssabral  3990  rabss  3999  ssrabeq  4010  uniiunlem  4012  sspsstri  4030  npss  4038  dfdif3  4042  raldifb  4072  uncom  4080  inass  4146  elsymdifxor  4176  nsspssun  4184  dfss4  4185  dfun2  4186  dfin2  4187  indi  4200  indifdir  4210  difin2  4216  reupick3  4240  eq0f  4255  neq0f  4256  eq0  4258  dfnf5  4288  rabn0  4293  csbab  4345  vss  4351  disj  4355  disjOLD  4356  disj3  4361  undisj1  4369  undisj2  4370  inundif  4385  undif  4388  absn  4543  rabsssn  4567  exsnrex  4578  euabsn2  4621  euabsn  4622  raldifsni  4688  tppreqb  4698  pwpw0  4706  prssg  4712  ssunsn  4721  preqsn  4752  pwpr  4794  dfuni2  4802  unissb  4832  elint2  4845  ssint  4854  uniintab  4876  dfiin2g  4919  iunn0  4952  iunxun  4979  iunxiun  4982  iinpw  4991  disjor  5010  disjxiun  5027  dftr2  5138  dftr5  5139  dftr3  5140  dftr4  5141  axrep6  5161  vnex  5182  inuni  5210  eusv2  5262  reusv2lem4  5267  rexxfr  5282  snelpw  5303  sspwb  5307  opthneg  5338  pwssun  5421  dfid3  5427  dffr2  5484  opthprc  5580  elxp3  5582  xpiundir  5587  elvv  5590  reliun  5653  inxp  5667  raliunxp  5674  cnvuni  5721  dmopab2rex  5750  dm0rn0  5759  elrn  5786  dfres3  5823  ssdmres  5841  elidinxp  5878  idinxpres  5881  dfima2  5898  args  5924  dffr3  5929  cotrg  5938  intasym  5942  asymref  5943  intirr  5945  xpnz  5983  xp11  5999  ssrnres  6002  xpimasn  6009  coiun  6076  coass  6085  cnvso  6107  elsnxp  6110  dffr4  6132  wfi  6149  dflim2  6215  orddif  6252  dffun2  6334  dffun6f  6338  dffun7  6351  dffun9  6353  funfn  6354  svrelfun  6396  mptfnf  6455  dffn2  6489  dffn3  6499  fint  6532  dffn4  6571  dff1o4  6598  brprcneu  6637  eqfnfv3  6781  fnreseql  6795  fsn  6874  ftpg  6895  abrexco  6981  imaiun  6982  dff13  6991  isof1oidb  7056  isof1oopb  7057  isocnv2  7063  mpo2eqb  7262  elovmpo  7370  sorpss  7434  abexex  7654  elxp6  7705  elxp7  7706  releldm2  7724  opiota  7739  fnmpo  7749  frxp  7803  cnvimadfsn  7822  mpoxneldm  7861  dftpos4  7894  wfrlem8  7945  wfrfun  7948  dfrecs3  7992  tfrlem7  8002  ondif1  8109  oarec  8171  oeeu  8212  0er  8309  eroveu  8375  erovlem  8376  elixpconst  8452  domen  8505  brsdom  8515  brdom2  8522  reuen1  8561  sbthlem10  8620  brsdom2  8625  xpf1o  8663  onfin2  8695  0sdom1dom  8700  modom  8703  unfi  8769  marypha2lem3  8885  wemapsolem  8998  elom3  9095  dfom5  9097  trcl  9154  epfrs  9157  rankf  9207  scottexs  9300  scott0s  9301  cplem1  9302  karden  9308  hta  9310  djuexb  9322  pm54.43lem  9413  alephsuc2  9491  iscard3  9504  aceq0  9529  aceq3lem  9531  dfac3  9532  dfac5lem2  9535  dfac5  9539  dfac7  9543  dfac12a  9559  kmlem12  9572  kmlem14  9574  kmlem15  9575  infmap2  9629  ackbij2  9654  dfacfin7  9810  ituniiun  9833  zorng  9915  brdom7disj  9942  entri2  9969  alephreg  9993  fpwwe2lem12  10052  fpwwe2lem13  10053  pwfseqlem1  10069  grutsk  10233  axgroth4  10243  grothprim  10245  grothtsk  10246  elni2  10288  ltsopi  10299  genpass  10420  psslinpr  10442  ltexprlem4  10450  ltresr  10551  1re  10630  infm3  11587  elnnz  11979  dfz2  11988  2rexuz  12288  nnwos  12303  eluz2b1  12307  qexALT  12351  elxr  12499  dflt2  12529  xrsupss  12690  xrinfmss  12691  elixx1  12735  elioo2  12767  elioopnf  12821  elicopnf  12823  elfz1  12890  fznn  12970  fzp1nel  12986  fznn0  12994  preduz  13024  prinfzo0  13071  injresinj  13153  nn0opthlem1  13624  faclbnd4lem1  13649  hashfxnn0  13693  hashprdifel  13755  hashgt23el  13781  hashfun  13794  hashf1  13811  fz1isolem  13815  f1oun2prg  14270  brtrclfv  14353  shftdm  14422  rediv  14482  imdiv  14489  rexanre  14698  caubnd  14710  climreu  14905  prodmo  15282  dvdslelem  15651  3dvdsdec  15673  3dvds2dec  15674  bitsval  15763  smueqlem  15829  algcvgblem  15911  lcmfunsnlem2  15974  isprm2  16016  isprm3  16017  isprm4  16018  pythagtriplem2  16144  elgz  16257  hashbc0  16331  0ram  16346  isstruct  16488  issect  17015  isfull2  17173  isfth2  17177  fucinv  17235  eldmcoa  17317  isdrs  17536  submacs  17983  isnsg4  18311  isgim  18394  gaorb  18429  oppgid  18476  oppgsubm  18482  oppgcntz  18484  ispgp  18709  efgsdm  18848  efgcpbllema  18872  iscyg2  18994  isring  19294  isirred2  19447  opprirred  19448  dfrhm2  19465  drngid2  19511  opprsubrg  19549  issdrg  19567  islmod  19631  lss1d  19728  islmhm  19792  islmim  19827  lbsextlem2  19924  lidlnz  19994  isnzr2  20029  dfprm2  20187  isphl  20317  elocv  20357  iunocv  20370  isobs  20409  islinds  20498  isassa  20545  1mavmul  21153  toprntopon  21530  isbasis3g  21554  fctop  21609  cctop  21611  isclo2  21693  restsn  21775  lmbr  21863  ist0-3  21950  2ndcdisj  22061  1stccnp  22067  islocfin  22122  1stckgenlem  22158  txbas  22172  ptbasin  22182  tx2cn  22215  fbfinnfr  22446  fbasrn  22489  filuni  22490  ufinffr  22534  fin1aufil  22537  rnelfmlem  22557  flimrest  22588  alexsubALTlem3  22654  alexsubALTlem4  22655  tgphaus  22722  istlm  22790  iscusp2  22908  metuel2  23172  isngp2  23203  isnlm  23281  isphtpc  23599  phtpcer  23600  om1elbas  23637  isclm  23669  iscvsp  23733  iscph  23775  iscau3  23882  minveclem3b  24032  elovolm  24079  ioombl1lem4  24165  dyaddisj  24200  vitali  24217  itg1climres  24318  itg2seq  24346  itg2monolem1  24354  itg2mono  24357  limcrcl  24477  lhop1  24617  itgsubst  24652  mdegleb  24665  isuc1p  24741  ismon1p  24743  plydivex  24893  ellogdm  25230  1cubr  25428  atandm2  25463  birthdaylem3  25539  dmarea  25543  dchrelbas2  25821  dchrelbas4  25827  axcontlem7  26764  nb3grpr  27172  nb3grpr2  27173  upgrwlkcompim  27432  wlkson  27446  wlkonprop  27448  wksonproplem  27494  ispth  27512  wwlknon  27643  wwlksnextinj  27685  wspthsnwspthsnon  27702  elwspths2spth  27753  rusgrnumwwlkl1  27754  clwwlkccatlem  27774  erclwwlkref  27805  frgr3v  28060  nmoubi  28555  nmobndseqi  28562  nmobndseqiALT  28563  minvecolem1  28657  isch2  29006  hlimreui  29022  isch3  29024  ocsh  29066  dfch2  29190  spanuni  29327  nonbooli  29434  5oalem7  29443  adjsym  29616  elbdop2  29654  dmadjss  29670  nmopub  29691  nmfnleub  29708  nmop0h  29774  pjssposi  29955  pjordi  29956  cvbr2  30066  cvnbtwn2  30070  mdsl2i  30105  cvmdi  30107  elat2  30123  atom1d  30136  chirredi  30177  cdj3i  30224  or3di  30231  opreu2reu1  30254  moel  30259  mo5f  30260  reuxfrdf  30262  rexunirn  30263  difrab2  30268  iuninc  30324  disjorf  30342  disjunsn  30357  rabfmpunirn  30416  aciunf1  30426  funcnv5mpt  30431  dfrp2  30517  eliccelico  30526  elicoelioo  30527  isomnd  30752  omndmul2  30763  isslmd  30880  islinds5  30983  ismxidl  31042  hasheuni  31454  pwsiga  31499  sigainb  31505  issros  31544  2ndmbfm  31629  omssubaddlem  31667  omssubadd  31668  sitgaddlemb  31716  eulerpartlemgvv  31744  eulerpartlemn  31749  probun  31787  ballotlem2  31856  ballotlemodife  31865  bnj252  32083  bnj253  32084  bnj255  32085  bnj345  32094  bnj133  32107  bnj976  32159  bnj1098  32165  bnj121  32252  bnj130  32256  bnj150  32258  bnj581  32290  bnj607  32298  bnj865  32305  bnj917  32316  bnj934  32317  bnj964  32325  bnj983  32333  bnj996  32338  bnj1021  32348  bnj1033  32351  bnj1047  32355  bnj1049  32356  bnj1090  32361  bnj1128  32372  bnj1175  32386  bnj1189  32391  bnj1253  32399  bnj1312  32440  exdifsn  32455  erdszelem9  32559  erdszelem10  32560  pconnconn  32591  cvmliftiota  32661  fmlaomn0  32750  fmla0disjsuc  32758  fmlasucdisj  32759  dmopab3rexdif  32765  elmthm  32936  nepss  33061  dfso2  33103  dfpo2  33104  elrn3  33111  imaindm  33135  elpotr  33139  dfon2lem5  33145  dfon2lem7  33147  dfon2lem8  33148  frpoind  33193  frind  33198  soseq  33209  elwlim  33223  wzel  33224  frrlem9  33244  elno3  33275  nosgnn0  33278  nosepon  33285  nocvxminlem  33360  scutcut  33379  scutbday  33380  dmscut  33385  scutf  33386  sltrec  33391  brtxp2  33455  brpprod3a  33460  eltrans  33465  dfon3  33466  dffix2  33479  dffun10  33488  elfuns  33489  brsingle  33491  brimg  33511  funpartfun  33517  funpartfv  33519  cgrxfr  33629  segletr  33688  outsideoftr  33703  neifg  33832  filnetlem4  33842  df3nandALT1  33860  bj-consensusALT  34025  bj-df-ifc  34026  bj-biexal3  34154  bj-nfnnfTEMP  34202  bj-denoteslem  34309  bj-denotes  34310  bj-ralvw  34319  bj-rexvw  34320  bj-rexcom4bv  34322  bj-rexcom4b  34323  bj-sbeq  34342  bj-inrab  34369  bj-rcleqf  34461  bj-dfmpoa  34533  bj-imdirco  34605  topdifinffinlem  34764  topdifinfeq  34767  relowlssretop  34780  relowlpssretop  34781  rdgeqoa  34787  domalom  34821  nlpineqsn  34825  fvineqsneq  34829  wl-ifpimpr  34883  wl-df3xor3  34887  wl-3xorbi  34890  wl-3xorbi2  34891  wl-2xor  34900  wl-2mintru2  34908  wl-dfclab  34993  wl-dfralsb  35002  wl-dfrexsb  35016  wl-dfrmosb  35018  wl-dfrmov  35019  wl-dfrabv  35027  rabiun  35030  phpreu  35041  fin2solem  35043  matunitlindflem2  35054  ptrest  35056  poimirlem25  35082  poimirlem27  35084  poimirlem30  35087  ismblfin  35098  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  itg2addnclem2  35109  fdc  35183  prdstotbnd  35232  isdrngo1  35394  ispridl  35472  ismaxidl  35478  impor  35519  selconj  35538  tradd  35543  scott0f  35607  inxpss3  35731  idinxpssinxp2  35735  idinxpssinxp3  35736  dfrel5  35763  ineleq  35768  moantr  35776  dfxrn2  35788  inxpxrn  35803  rnxrnres  35807  1cossres  35834  cocossss  35841  cossssid4  35870  cossssid5  35871  cosscnvssid5  35878  cossid  35880  dfssr2  35899  cnvrefrelcoss2  35933  cosselcnvrefrels2  35934  eqvrelcoss  36012  eqvrelcoss2  36014  dfcoeleqvrel  36017  refrelredund4  36030  cnvepresdmqs  36047  dfmember  36066  dfdisjALTV  36106  dfeldisj3  36112  dfeldisj4  36113  dfeldisj5  36114  prter1  36175  islshp  36275  islshpat  36313  lcvbr2  36318  lcvnbtwn2  36323  cvrnbtwn3  36572  isatl  36595  ishlat1  36648  ishlat2  36649  cvrat4  36739  pmapglbx  37065  lhpexle3  37308  dib1dim  38461  diblsmopel  38467  lcfls1lem  38830  prjsperref  39598  prjspeclsp  39604  rexrabdioph  39733  dford4  39968  isdomn3  40146  ifpdfor2  40167  ifpdfan2  40169  ifpdfor  40171  ifpdfan  40172  ifpnot23b  40188  ifpnot23c  40190  ifpnot23d  40191  ifpim123g  40206  ifpbibib  40216  clss2lem  40309  imaiun1  40350  coiun1  40351  brfvrcld2  40391  iunrelexp0  40401  brtrclfv2  40426  snhesn  40485  dffrege76  40638  frege97  40659  frege98  40660  frege109  40671  frege110  40672  dffrege115  40677  frege131  40693  frege133  40695  ntrneineine1lem  40785  ntrneiel2  40787  ntrneiiso  40792  gneispace3  40834  scotteld  40952  ismnuprim  41000  pm11.52  41089  pm11.58  41092  pm13.192  41112  impexpdcom  41219  sbc3or  41236  opelopab4  41255  uunT12p1  41504  uunT12p2  41505  uunT12p3  41506  uun2221  41517  uun2221p1  41518  uun2221p2  41519  undif3VD  41586  ndisj2  41683  nssrex  41720  rabssf  41752  bothtbothsame  43490  bothfbothsame  43491  aiffbtbat  43499  reuabaiotaiota  43642  2reu8i  43667  2reuimp0  43668  ichn  43971  dfodd2  44152  dfeven5  44182  dfodd7  44183  1nevenALTV  44207  oddprmne2  44231  isrng  44498  isrnghm  44514  islindeps2  44890  isldepslvec2  44892  line2xlem  45165  setrec1lem3  45217  aacllem  45327
  Copyright terms: Public domain W3C validator