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  427  dfbi2  663  pm5.32  671  imdistan  727  bianass  877  imimorb  957  nbi2  972  pm5.6  989  mpbiran  991  mpbiran2  992  biluk  1012  casesifp  1064  3ancoma  1084  3ancomb  1086  3anrev  1091  an3andi  1592  nancom  1597  nanbi  1601  xorneg  1623  cadan  1695  cadcomb  1699  nic-ax  1745  nic-axALT  1746  nf3  1859  19.43  1957  19.3v  2061  nf5  2261  nf6  2262  sb6x  2519  sb5f  2521  sb3an  2535  sbequ8ALT  2542  sb5  2565  sbhb  2573  sbnf2  2574  sbcom2  2580  eu1  2646  cleqh  2860  clelab  2884  necon3bii  2982  neor  3021  neorian  3024  r2allem  3073  r19.23t  3157  r19.26-3  3202  r19.26m  3203  r19.43  3229  rabid2  3255  rabid2f  3256  eqvf  3342  isset  3345  ralv  3357  rexv  3358  reuv  3359  rmov  3360  rexcom4b  3365  ceqsex4v  3385  ceqsex8v  3387  ceqsrexv  3473  rabtru  3499  ralrab2  3511  rexrab2  3513  reu2  3533  reu3  3535  reueq  3543  2reuswap  3549  reuind  3550  2reu5lem3  3554  sbc3an  3633  rmo2  3665  dfss2  3730  dfss3  3731  dfss3f  3734  ssabral  3812  rabss  3818  ssrabeq  3829  uniiunlem  3831  sspsstri  3849  npss  3857  dfdif3  3861  raldifb  3891  uncom  3898  inass  3964  symdifass  3994  nsspssun  3998  dfss4  3999  dfun2  4000  dfin2  4001  indi  4014  indifdir  4024  difin2  4031  reupick3  4053  eq0f  4066  neq0f  4067  n0fOLD  4069  rabn0  4099  csbab  4149  vss  4153  disj  4158  disj3  4162  undisj1  4171  undisj2  4172  inundif  4188  undif  4191  rabeqsn  4356  rabsssn  4357  exsnrex  4363  euabsn2  4402  euabsn  4403  raldifsni  4468  tppreqb  4479  pwpw0  4487  prssg  4493  ssunsn  4503  preqsn  4538  pwpr  4580  dfuni2  4588  unissb  4619  elint2  4632  ssint  4643  uniintab  4665  iuneq12df  4694  dfiin2g  4703  iunn0  4730  iunxun  4755  iunxiun  4758  iinpw  4767  disjor  4784  disjxiun  4799  dftr2  4904  dftr5  4905  dftr3  4906  dftr4  4907  vprc  4946  inuni  4973  eusv2  5012  reusv2lem4  5019  rexxfr  5035  snelpw  5060  sspwb  5064  opthneg  5096  pwssun  5168  dfid3  5173  dffr2  5229  opthprc  5322  elxp3  5324  xpiundir  5329  elvv  5332  brinxp2  5335  relsnOLD  5381  reliun  5393  inxp  5408  raliunxp  5415  cnvuni  5462  dm0rn0  5495  elrn  5519  dfres3  5554  ssdmres  5576  dfres2  5609  dfima2  5624  args  5649  dffr3  5654  cotrg  5663  intasym  5667  asymref  5668  intirr  5670  cnv0OLD  5692  xpnz  5709  xp11  5725  xpimasn  5735  resco  5798  rnco  5800  coiun  5804  coass  5813  cnvso  5833  elsnxp  5836  elsnxpOLD  5837  dffr4  5855  wfi  5872  dflim2  5940  orddif  5979  dfiota2  6011  dffun2  6057  dffun6f  6061  dffun7  6074  dffun9  6076  funfn  6077  svrelfun  6120  mptfnf  6174  dffn2  6206  dffn3  6213  fint  6243  dffn4  6280  dff1o4  6304  brprcneu  6343  eqfnfv3  6474  fnreseql  6488  fsn  6563  ftpg  6584  abrexco  6663  imaiun  6664  dff13  6673  isof1oidb  6735  isof1oopb  6736  isocnv2  6742  mpt22eqb  6932  elovmpt2  7042  sorpss  7105  abexex  7314  elxp6  7365  elxp7  7366  releldm2  7383  opiota  7394  fnmpt2  7404  frxp  7453  cnvimadfsn  7470  mpt2xneldm  7505  dftpos4  7538  wfrlem8  7589  wfrfun  7592  dfrecs3  7636  tfrlem7  7646  ondif1  7748  oarec  7809  oeeu  7850  0er  7946  eroveu  8007  erovlem  8008  map0e  8059  elixpconst  8080  domen  8132  brsdom  8142  brdom2  8149  reuen1  8188  sbthlem10  8242  brsdom2  8247  xpf1o  8285  onfin2  8315  0sdom1dom  8321  modom  8324  unfi  8390  marypha2lem3  8506  wemapsolem  8618  sucprcreg  8669  elom3  8716  dfom5  8718  trcl  8775  epfrs  8778  rankf  8828  scottexs  8921  scott0s  8922  cplem1  8923  karden  8929  hta  8931  pm54.43lem  9013  alephsuc2  9091  iscard3  9104  aceq0  9129  aceq3lem  9131  dfac3  9132  dfac5lem2  9135  dfac5  9139  dfac7  9144  dfac12a  9160  kmlem12  9173  kmlem14  9175  kmlem15  9176  infmap2  9230  ackbij2  9255  dfacfin7  9411  ituniiun  9434  zorng  9516  brdom7disj  9543  entri2  9570  alephreg  9594  fpwwe2lem12  9653  fpwwe2lem13  9654  pwfseqlem1  9670  grutsk  9834  axgroth4  9844  grothprim  9846  grothtsk  9847  elni2  9889  ltsopi  9900  genpass  10021  psslinpr  10043  ltexprlem4  10051  ltresr  10151  1re  10229  infm3  11172  elnnz  11577  dfz2  11585  2rexuz  11931  nnwos  11946  eluz2b1  11950  qexALT  11994  elxr  12141  dflt2  12172  xrsupss  12330  xrinfmss  12331  elixx1  12375  elioo2  12407  elioopnf  12458  elicopnf  12460  elfz1  12522  fznn  12599  fzp1nel  12615  fznn0  12623  preduz  12653  prinfzo0  12699  injresinj  12781  nn0opthlem1  13247  faclbnd4lem1  13272  hashfxnn0  13316  hashfOLD  13318  hashprdifel  13376  hashfun  13414  hashf1  13431  fz1isolem  13435  f1oun2prg  13860  brtrclfv  13940  shftdm  14008  rediv  14068  imdiv  14075  rexanre  14283  caubnd  14295  climreu  14484  prodmo  14863  dvdslelem  15231  3dvdsdec  15254  3dvdsdecOLD  15255  3dvds2dec  15256  3dvds2decOLD  15257  bitsval  15346  smueqlem  15412  algcvgblem  15490  lcmfunsnlem2  15553  isprm2  15595  isprm3  15596  isprm4  15597  pythagtriplem2  15722  elgz  15835  hashbc0  15909  0ram  15924  isstruct  16070  issect  16612  isfull2  16770  isfth2  16774  fucinv  16832  eldmcoa  16914  isdrs  17133  fpwipodrs  17363  submacs  17564  isnsg4  17836  isgim  17903  gaorb  17938  oppgid  17984  oppgsubm  17990  oppgcntz  17992  ispgp  18205  efgsdm  18341  efgcpbllema  18365  iscyg2  18482  isring  18749  isirred2  18899  opprirred  18900  dfrhm2  18917  drngid2  18963  opprsubrg  19001  islmod  19067  lss1d  19163  islmhm  19227  islmim  19262  lbsextlem2  19359  lidlnz  19428  lidldvgen  19455  isnzr2  19463  isassa  19515  dfprm2  20042  isphl  20173  elocv  20212  iunocv  20225  isobs  20264  islinds  20348  1mavmul  20554  isbasis3g  20953  fctop  21008  cctop  21010  isclo2  21092  restsn  21174  lmbr  21262  ist0-3  21349  2ndcdisj  21459  1stccnp  21465  islocfin  21520  1stckgenlem  21556  txbas  21570  ptbasin  21580  tx2cn  21613  fbfinnfr  21844  fbasrn  21887  filuni  21888  ufinffr  21932  fin1aufil  21935  rnelfmlem  21955  flimrest  21986  alexsubALTlem3  22052  alexsubALTlem4  22053  tgphaus  22119  istlm  22187  iscusp2  22305  metuel2  22569  isngp2  22600  isnlm  22678  elcncf1di  22897  isphtpc  22992  phtpcer  22993  om1elbas  23030  isclm  23062  iscvsp  23126  iscph  23168  iscau3  23274  minveclem3b  23397  elovolm  23441  ioombl1lem4  23527  dyaddisj  23562  vitali  23579  itg1climres  23678  itg2seq  23706  itg2monolem1  23714  itg2mono  23717  limcrcl  23835  lhop1  23974  itgsubst  24009  mdegleb  24021  isuc1p  24097  ismon1p  24099  plydivex  24249  ellogdm  24582  1cubr  24766  atandm2  24801  birthdaylem3  24877  dmarea  24881  dchrelbas2  25159  dchrelbas4  25165  axcontlem7  26047  nb3grpr  26480  nb3grpr2  26481  upgrwlkcompim  26747  wlkson  26760  wlkonprop  26762  wksonproplem  26809  ispth  26827  wwlknon  26961  wwlknonOLD  26963  wwlksnextinj  27015  wspthsnwspthsnon  27032  elwspths2spth  27087  rusgrnumwwlkl1  27088  clwwlkccatlem  27110  erclwwlkref  27141  frgr3v  27427  nmoubi  27934  nmobndseqi  27941  nmobndseqiALT  27942  minvecolem1  28037  isch2  28387  hlimreui  28403  isch3  28405  ocsh  28449  dfch2  28573  spanuni  28710  nonbooli  28817  5oalem7  28826  adjsym  28999  elbdop2  29037  dmadjss  29053  nmopub  29074  nmfnleub  29091  nmop0h  29157  pjssposi  29338  pjordi  29339  cvbr2  29449  cvnbtwn2  29453  mdsl2i  29488  cvmdi  29490  elat2  29506  atom1d  29519  chirredi  29560  cdj3i  29607  or3di  29614  moel  29630  mo5f  29631  2reuswap2  29634  rexunirn  29637  difrab2  29644  difininv  29659  iuneq12daf  29678  iuninc  29684  disjorf  29697  disjunsn  29712  rabfmpunirn  29760  aciunf1  29770  funcnv5mpt  29776  dfrp2  29839  eliccelico  29846  elicoelioo  29847  isomnd  30008  omndmul2  30019  isslmd  30062  hasheuni  30454  pwsiga  30500  sigainb  30506  issros  30545  2ndmbfm  30630  omssubaddlem  30668  omssubadd  30669  sitgaddlemb  30717  eulerpartlemgvv  30745  eulerpartlemn  30750  probun  30788  ballotlem2  30857  ballotlemodife  30866  bnj252  31076  bnj253  31077  bnj255  31078  bnj345  31087  bnj133  31100  bnj976  31153  bnj1098  31159  bnj121  31245  bnj130  31249  bnj150  31251  bnj581  31283  bnj607  31291  bnj865  31298  bnj917  31309  bnj934  31310  bnj964  31318  bnj983  31326  bnj996  31330  bnj1021  31339  bnj1033  31342  bnj1047  31346  bnj1049  31347  bnj1090  31352  bnj1128  31363  bnj1175  31377  bnj1189  31382  bnj1253  31390  bnj1312  31431  erdszelem9  31486  erdszelem10  31487  pconnconn  31518  cvmliftiota  31588  elmthm  31778  nepss  31904  dfso2  31949  dfpo2  31950  elrn3  31957  imaindm  31985  elpotr  31989  dfon2lem5  31995  dfon2lem7  31997  dfon2lem8  31998  frpoind  32044  frind  32047  soseq  32058  elwlim  32072  wzel  32073  frrlem5c  32090  elno3  32112  nosgnn0  32115  nosepon  32122  nocvxminlem  32197  scutcut  32216  scutbday  32217  dmscut  32222  scutf  32223  sltrec  32228  brtxp2  32292  brpprod3a  32297  eltrans  32302  dfon3  32303  dffix2  32316  dffun10  32325  elfuns  32326  brsingle  32328  brimg  32348  funpartfun  32354  funpartfv  32356  cgrxfr  32466  segletr  32525  outsideoftr  32540  neifg  32670  filnetlem4  32680  df3nandALT1  32700  bj-consensusALT  32867  bj-biexal3  33002  bj-sb5  33072  bj-ralvw  33169  bj-rexvwv  33170  bj-rexcom4bv  33175  bj-rexcom4b  33176  bj-sbeq  33200  bj-inrab  33227  bj-xpima1snALT  33248  bj-dfmpt2a  33375  topdifinffinlem  33504  topdifinfeq  33507  relowlssretop  33520  relowlpssretop  33521  rdgeqoa  33527  wl-dfnan2  33607  wl-nannan  33609  rabiun  33693  phpreu  33704  fin2solem  33706  matunitlindflem2  33717  ptrest  33719  poimirlem25  33745  poimirlem27  33747  poimirlem30  33750  ismblfin  33761  ovoliunnfl  33762  voliunnfl  33764  volsupnfl  33765  itg2addnclem2  33773  fdc  33852  prdstotbnd  33904  isdrngo1  34066  ispridl  34144  ismaxidl  34150  impor  34191  selconj  34213  tradd  34218  scott0f  34288  biancom  34318  inxpss3  34406  idinxpssinxp2  34411  idinxpssinxp3  34412  dfrel5  34435  ineleq  34440  moantr  34448  dfxrn2  34459  inxpxrn  34474  rnxrnres  34478  1cossres  34505  cocossss  34512  cossssid4  34541  cossssid5  34542  cosscnvssid5  34549  cossid  34551  dfssr2  34570  cnvrefrelcoss2  34604  cosselcnvrefrels2  34605  prter1  34666  islshp  34767  islshpat  34805  lcvbr2  34810  lcvnbtwn2  34815  cvrnbtwn3  35064  isatl  35087  ishlat1  35140  ishlat2  35141  cvrat4  35230  pmapglbx  35556  lhpexle3  35799  dib1dim  36954  diblsmopel  36960  lcfls1lem  37323  rexrabdioph  37858  dford4  38096  issdrg  38267  isdomn3  38282  ifpdfor2  38305  ifpdfan2  38307  ifpdfor  38309  ifpdfan  38310  ifpdfbi  38318  ifpnot23b  38327  ifpnot23c  38329  ifpnot23d  38330  ifpim123g  38345  ifpbibib  38355  clss2lem  38418  imaiun1  38443  coiun1  38444  brfvrcld2  38484  iunrelexp0  38494  brtrclfv2  38519  snhesn  38580  dffrege76  38733  frege97  38754  frege98  38755  frege109  38766  frege110  38767  dffrege115  38772  frege131  38788  frege133  38790  ntrneineine1lem  38882  ntrneiel2  38884  ntrneiiso  38889  gneispace3  38931  pm11.52  39086  pm11.58  39090  pm13.192  39111  conss34OLD  39146  impexpdcom  39221  sbc3or  39238  opelopab4  39267  uunT12p1  39527  uunT12p2  39528  uunT12p3  39529  uun2221  39540  uun2221p1  39541  uun2221p2  39542  undif3VD  39615  ndisj2  39715  nssrex  39757  rabssf  39799  bothtbothsame  41570  bothfbothsame  41571  aiffbtbat  41579  rmoanim  41683  2rmoswap  41688  dfodd2  42057  dfeven5  42086  dfodd7  42087  1nevenALTV  42110  oddprmne2  42132  isrng  42384  isrnghm  42400  islindeps2  42780  isldepslvec2  42782  setrec1lem3  42944  aacllem  43058
  Copyright terms: Public domain W3C validator