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

Theorem mpbiri 233
Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
mpbiri.min
mpbiri.maj
Assertion
Ref Expression
mpbiri

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3
21a1i 11 . 2
3 mpbiri.maj . 2
42, 3mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  dedt  957  spei  2012  nfald2  2073  nfabd2  2640  dedhb  3269  sbceqal  3383  ssdifeq0  3910  r19.2zb  3919  dedth  3993  pwidg  4025  elpr2  4048  snidg  4055  exsnrex  4067  ifpr  4077  rabrsn  4100  prid1g  4136  pwpw0  4178  sssn  4188  preqr1  4204  pwsnALT  4244  unimax  4285  intmin3  4315  syl6eqbr  4489  intabs  4613  pwnss  4617  0inp0  4624  copsexg  4737  copsexgOLD  4738  euotd  4753  elopab  4760  epelg  4797  ord0eln0  4937  sucidg  4961  nsuceq0  4963  onun2i  4998  elvvuni  5065  posn  5073  frsn  5075  eqrelriv  5101  relopabi  5133  opabid2  5137  ididg  5161  iss  5326  funopg  5625  fn0  5705  f00  5772  f0bi  5773  f1o00  5853  fo00  5854  brprcneu  5864  dffn5  5918  fsn  6069  fnsnb  6090  fconstfvOLD  6134  eufnfv  6146  f1eqcocnv  6204  nfriotad  6265  riotaprop  6281  oprabid  6323  elrnmpt2  6415  ov6g  6440  ovelrn  6451  caovmo  6512  offn  6551  caofinvl  6567  fr3nr  6615  onprc  6620  ordeleqon  6624  onint0  6631  0elsuc  6670  onuninsuci  6675  orduninsuc  6678  ordzsl  6680  onzsl  6681  tfinds  6694  limomss  6705  limom  6715  peano5  6723  xpexr  6740  eqop2  6841  1stconst  6888  2ndconst  6889  funsssuppss  6945  dftpos3  6992  dftpos4  6993  oawordeulem  7222  omwordi  7239  nnmwordi  7303  riiner  7403  ecopover  7434  map0g  7478  mapsn  7480  elixpsn  7528  en0  7598  en1  7602  fiprc  7617  sbthlem2  7648  sbthlem4  7650  sbthlem5  7651  nneneq  7720  sdom1  7739  fineqvlem  7754  nfielex  7768  findcard  7779  findcard2  7780  elfiun  7910  marypha1lem  7913  oicl  7975  oif  7976  oion  7982  hartogslem1  7988  hartogs  7990  wemapso2  8000  card2on  8001  0wdom  8017  brwdom2  8020  sucprcregOLD  8047  inf3lem6  8071  noinfepOLD  8098  cantnflem3  8131  cantnflem4  8132  cantnflem3OLD  8153  cantnflem4OLD  8154  wemapwe  8160  wemapweOLD  8161  cnfcom  8165  cnfcomOLD  8173  tctr  8192  r1tr  8215  r1rankidb  8243  r1pw  8284  scottex  8324  scott0  8325  bnd2  8332  tskwe  8352  oncard  8362  cardlim  8374  harsdom  8397  en2eleq  8407  dfac8alem  8431  cardaleph  8491  iunfictbso  8516  infmap2  8619  ackbij1lem18  8638  cff  8649  cfsuc  8658  cff1  8659  cflim2  8664  cfss  8666  sdom2en01  8703  infpssrlem4  8707  fin23lem7  8717  fin23lem11  8718  isfin2-2  8720  fin23lem26  8726  fin23lem19  8737  fin23lem17  8739  isf34lem2  8774  isf34lem4  8778  fin1a2lem6  8806  fin1a2lem10  8810  fin1a2lem12  8812  itunifn  8818  hsmexlem1  8827  axcc2lem  8837  dcomex  8848  axdc3lem4  8854  ondomon  8959  konigthlem  8964  pwcfsdom  8979  cfpwsdom  8980  axpowndlem3  8996  axpowndlem3OLD  8997  canth4  9046  canthnumlem  9047  canthwelem  9049  canthwe  9050  canthp1lem2  9052  pwfseqlem4  9061  pwfseqlem5  9062  gchaleph  9070  gch2  9074  winainflem  9092  0tsk  9154  rankcf  9176  tskcard  9180  gruina  9217  grutsk  9221  tskmid  9239  indpi  9306  nqereu  9328  mulcanenq  9359  recmulnq  9363  archnq  9379  ltsopr  9431  1ne0sr  9494  0idsr  9495  00sr  9497  leid  9701  lelttric  9712  divcan3  10256  lemul1a  10421  nn1suc  10582  nn0n0n1ge2b  10885  nn0lt10b  10950  nn0ind-raph  10989  elnn1uz2  11187  indstr2  11189  uzsupss  11203  rpnnen1lem4  11240  rpnnen1lem5  11241  xrnemnf  11357  xrnepnf  11358  mnfltxr  11365  nn0pnfge0  11370  xrlttri  11374  xrlttr  11375  xrleid  11385  qbtwnxr  11428  xmullem2  11486  xlemul1a  11509  xrub  11532  ixxun  11574  fztpval  11770  fseq1p1m1  11781  elfznelfzob  11916  ltweuz  12072  fzfi  12082  fsuppmapnn0fiubex  12098  ser0f  12160  0exp  12201  faclbnd4lem1  12371  bcn1  12391  hashnemnf  12417  hashv01gt1  12418  hashle00  12465  hashgt12el2  12482  hashmap  12493  hashpw  12494  hashf1  12506  fz1isolem  12510  hash2prd  12518  hash2prv  12525  0wrd0  12566  wrdlen1  12579  ccatvalfn  12599  swrdlen  12650  swrdvalfn  12663  swrdspsleq  12673  cats1un  12701  wrdind  12702  wrd2ind  12703  swrdccatin1  12708  repswsymballbi  12752  cshw1  12790  scshwfzeqfzo  12794  sqr0lem  13074  sqrtsq  13103  mptfzshft  13593  fsumrev  13594  prodf1f  13701  fprodrev  13781  egt2lt3  13939  0dvds  14004  bitsp1o  14083  gcddvds  14153  bezout  14180  1nprm  14222  prmind2  14228  rpdvds  14265  pcpre1  14366  vdwapf  14490  vdwapid1  14493  ram0  14540  ramz  14543  cshws0  14586  prmlem0  14591  strle1  14728  restsspw  14829  prdsdsfn  14862  imasdsfn  14911  imasaddfnlem  14925  imasvscafn  14934  xpscfv  14959  xpsfrnel  14960  isacs1i  15054  cidfn  15076  comffn  15100  isoval  15159  sscres  15192  cofucl  15257  idffth  15302  ressffth  15307  catcoppccl  15435  1stfcl  15466  2ndfcl  15467  prfcl  15472  evlfcl  15491  curf1cl  15497  curfcl  15501  hofcl  15528  yonedainv  15550  pospo  15603  lubfun  15610  glbfun  15623  joindmss  15637  meetdmss  15651  ipopos  15790  acsficl2d  15806  dirref  15865  mgmidcl  15892  mgmlrid  15893  cntzssv  16366  symggrp  16425  symgid  16426  idresperm  16434  pmtrfmvdn0  16487  symggen  16495  psgnunilem1  16518  psgnprfval  16546  slwpgp  16633  frgpmhm  16783  frgpuptinv  16789  frgpup3lem  16795  gsumzoppg  16967  gsumcom2  17003  abv0  17480  rrgsupp  17939  psrvscafval  18043  psrridm  18058  psrridmOLD  18059  ltbwe  18137  psrbag0  18159  psrbagsn  18160  subrgascl  18163  zrhrhm  18549  psgnodpmr  18626  frlmphl  18812  ellspd  18836  ellspdOLD  18837  mattpostpos  18956  mavmul0  19054  mavmul0g  19055  mdet0f1o  19095  m1detdiag  19099  m2detleiblem5  19127  m2detleiblem6  19128  m2detleiblem3  19131  m2detleiblem4  19132  maducoeval2  19142  d1mat2pmat  19240  chpmat1dlem  19336  chpmat1d  19337  baspartn  19455  eltg3  19463  fctop  19505  cctop  19507  discld  19590  mretopd  19593  neipeltop  19630  neitr  19681  restcls  19682  ordtbaslem  19689  ordtuni  19691  idcn  19758  cnrmi  19861  cmpsublem  19899  cmpsub  19900  tgcmp  19901  uncmp  19903  hauscmplem  19906  cmpfi  19908  bwth  19910  bwthOLD  19911  1stcrestlem  19953  disllycmp  19999  dis1stc  20000  refref  20014  kgeni  20038  1stckgenlem  20054  kqffn  20226  snfil  20365  filcon  20384  cfinfil  20394  ufileu  20420  filufint  20421  fixufil  20423  cfinufil  20429  ufilen  20431  fin1aufil  20433  fmf  20446  rnelfm  20454  flimclslem  20485  hauspwpwf1  20488  supnfcls  20521  flimfnfcls  20529  fclscmp  20531  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALT  20551  ptcmplem1  20552  cnextrel  20563  tsmsfbas  20626  ustref  20721  trust  20732  restutop  20740  isusp  20764  xmet0  20845  imasdsf1olem  20876  blfvalps  20886  blfps  20909  blf  20910  restmetu  21090  dscmet  21093  isngp2  21117  nm0  21146  nrginvrcn  21200  nmoix  21236  qdensere  21277  iccconn  21335  iccpnfcnv  21444  xrhmeo  21446  lebnumlem3  21463  cmetss  21753  bcthlem5  21767  rrxmfval  21833  minveclem3b  21843  cniccbdd  21873  ovolicc2lem4  21931  iunmbl  21963  ioorinv  21985  ioorcl  21986  i1f1lem  22096  limcvallem  22275  ellimc2  22281  limccnp  22295  limccnp2  22296  limcco  22297  perfdvf  22307  recnprss  22308  fncpn  22336  dvcmulf  22348  c1lip1  22398  lhop2  22416  q1pcl  22556  r1pdeglt  22559  ply1remlem  22563  plyssc  22597  ulm0  22786  cxpeq0  23059  cxplea  23077  asinlem  23199  isppw2  23389  muval2  23408  dchrfi  23530  dchrpt  23542  bposlem6  23564  lgsdir2lem2  23599  lgsqr  23621  2sqlem7  23645  2sqlem11  23650  chtppilim  23660  tgldimor  23893  tglnfn  23934  tglnunirn  23935  mircinv  24048  perpln1  24087  perpln2  24088  lmiisolem  24161  xmstrkgc  24189  axcgrtr  24218  axsegconlem9  24228  axlowdimlem5  24249  axlowdimlem17  24261  axlowdim1  24262  uhgra0  24309  uhgra0v  24310  umgra0  24325  usgra0  24370  usgra0v  24371  usgraedg4  24387  usgra1v  24390  nb3graprlem1  24451  cusgra1v  24461  cusgraexilem2  24467  uvtx01vtx  24492  wlkcomp  24525  wlkntrl  24564  0spth  24573  1pthonlem1  24591  2pthlem1  24597  usgra2wlkspthlem1  24619  3v3e3cycl1  24644  constr3trllem1  24650  constr3pthlem3  24657  4cycl4v4e  24666  4cycl4dv  24667  0conngra  24674  wwlkn0s  24705  clwlkcomp  24763  frgra0v  24993  frgra1v  24998  1vwmgra  25003  vdgfrgragt2  25027  frgrancvvdeqlem3  25032  frgrawopreg1  25050  frgrawopreg2  25051  2spot0  25064  ex-opab  25153  grpoinvf  25242  ismgmOLD  25322  rngomndo  25423  nvmid  25560  nmlnoubi  25711  hiidrcl  26012  hsn0elch  26166  shjshseli  26411  cmbr4i  26519  dfiop2  26672  kbpj  26875  nmopun  26933  adjeq0  27010  kbass2  27036  pjssdif1i  27094  pjinvari  27110  pjcmul2i  27121  pj3i  27127  stge1i  27157  stle0i  27158  sumdmdlem2  27338  dmdbr6ati  27342  dmdbr7ati  27343  rabsnel  27402  disjdifprg  27436  ofoprabco  27505  fpwrelmapffslem  27555  xrlelttric  27572  iundisj2cnt  27604  nn0min  27611  xrge0tsmsbi  27776  locfinref  27844  dispcmp  27862  pstmxmet  27876  xrge0iifcnv  27915  xrge0iif1  27920  qqhre  27998  esumcl  28043  esumpr2  28074  esumpinfval  28079  esumpcvgval  28084  ofcfn  28099  pwsiga  28130  prsiga  28131  sigainb  28136  measiuns  28188  relfae  28219  sitgf  28289  eulerpartgbij  28311  sgnmulsgn  28488  sgnmulsgp  28489  signswch  28518  signslema  28519  signstlen  28524  subfacp1lem5  28628  erdszelem8  28642  kur14lem1  28650  indispcon  28679  cvmsss2  28719  msubrn  28889  relexpsucr  29053  dfpo2  29184  dfon2lem7  29221  wfrlem4  29346  wfrlem14  29356  frrlem6  29396  nosgnn0i  29419  nobndlem2  29453  nobndlem4  29455  nobndlem5  29456  nobndlem6  29457  brbigcup  29548  elsingles  29568  fnimage  29579  funpartlem  29592  dfrdg4  29600  imagesset  29603  altopthsn  29611  elaltxp  29625  ellines  29802  linethru  29803  rankeq1o  29828  elhf2  29832  hfninf  29843  limsucncmpi  29910  volsupnfl  30059  cnambfre  30063  dvasin  30103  dvacos  30104  nn0prpwlem  30140  fneref  30168  neibastop2lem  30178  sdclem2  30235  sstotbnd2  30270  ssbnd  30284  grpokerinj  30347  isdrngo1  30359  ac6s6  30580  prtlem12  30608  elrfirn  30627  ismrcd1  30630  istopclsd  30632  rabren3dioph  30749  jm2.17b  30899  jm2.22  30937  jm2.23  30938  ttac  30978  pw2f1ocnv  30979  dnnumch1  30990  hbtlem5  31077  mncn0  31088  aaitgo  31111  rngunsnply  31122  ssrecnpr  31188  seff  31189  sblpnf  31190  lcmdvds  31214  nzss  31222  dvconstbi  31239  ipo0  31358  ifr0  31359  addrfn  31381  subrfn  31382  mulvfn  31383  refsum2cnlem1  31412  ellimciota  31620  dvmptconst  31710  dvmptidg  31712  dvmulcncf  31722  dvdivcncf  31724  stoweidlem26  31808  stoweidlem50  31832  stoweidlem57  31839  2ffzoeq  32341  uhguhgra  32372  uhg0e  32376  uhgres  32379  fusgraimpcl  32427  fusgraimpclALT  32429  0mgm  32462  nnsgrpmgm  32504  fnhomeqhomf  32564  estrchomfn  32641  funcestrcsetclem4  32649  funcestrcsetclem7  32652  equivestrcsetc  32658  funcsetcestrclem4  32664  funcsetcestrclem7  32667  c0snmhm  32721  rngchomffvalOLD  32803  funcringcsetcOLD2lem4  32847  funcringcsetclem4OLD  32870  srhmsubc  32884  rhmsubclem1  32894  srhmsubcOLD  32903  rhmsubcOLDlem1  32913  mapsnop  32934  zlmodzxzldeplem4  33104  bnj145OLD  33782  bnj216  33787  bnj151  33935  bnj517  33943  bnj970  34005  bnj1145  34049  bnj1498  34117  bj-dedthm  34161  bj-speiv  34285  bj-exlimmpbir  34479  bj-snglex  34531  bj-inftyexpidisj  34613  riotasv2d  34688  lkrscss  34823  islshpkrN  34845  isline  35463  ispointN  35466  0psubN  35473  linepsubN  35476  atpsubN  35477  cdlemk36  36639  diafn  36761  dibfna  36881  dibvalrel  36890  dicvalrelN  36912  diclspsn  36921  dihvalrel  37006  dih1  37013  lclkrlem1  37233  lclkr  37260  mapd1o  37375  mapdin  37389  hdmapfnN  37559  hgmapfnN  37618
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 185
  Copyright terms: Public domain W3C validator