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

Theorem mpbiri 247
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 246 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  dedt  1025  dedtOLD  1028  spei  2249  nfald2  2319  nfabd2  2770  raleleqALT  3134  dedhb  3343  sbceqal  3454  ssdifeq0  4003  r19.2zb  4013  dedth  4089  pwidg  4121  elpr2  4147  elpr2OLD  4148  snidg  4153  exsnrex  4168  ifpr  4180  rabrsn  4203  prid1g  4239  tpid3g  4248  pwpw0  4284  sssn  4298  preqr1OLD  4320  elpreqpr  4334  pwsnALT  4367  unimax  4409  intmin3  4440  syl6eqbr  4622  intabs  4752  pwnss  4756  0inp0  4763  copsexg  4882  euotd  4900  elopab  4908  epelg  4950  elvvuni  5102  posn  5110  frsn  5112  eqrelriv  5136  relopabiALT  5168  opabid2  5173  ididg  5197  iss  5367  ord0eln0  5696  sucidg  5720  nsuceq0  5722  onun2i  5760  funopg  5836  fn0  5924  f00  6000  f0bi  6001  f10d  6082  f1o00  6083  fo00  6084  brprcneu  6096  dffn5  6151  fsn  6308  funop  6320  funsndifnop  6321  funsneqopsn  6322  fnsnb  6337  eufnfv  6395  f1eqcocnv  6456  nfriotad  6519  riotaprop  6534  oprabid  6576  elrnmpt2  6671  ov6g  6696  ovelrn  6708  caovmo  6769  offn  6806  caofinvl  6822  fr3nr  6871  onprc  6876  ordeleqon  6880  onint0  6888  0elsuc  6927  onuninsuci  6932  orduninsuc  6935  ordzsl  6937  onzsl  6938  tfinds  6951  limomss  6962  limom  6972  peano5  6981  xpexr  6999  eqop2  7100  1stconst  7152  2ndconst  7153  funsssuppss  7208  dftpos3  7257  dftpos4  7258  wfrlem4  7305  wfrlem14  7315  oawordeulem  7521  omwordi  7538  nnmwordi  7602  riiner  7707  ecopover  7738  ecopoverOLD  7739  map0g  7783  mapsn  7785  elixpsn  7833  en0  7905  en1  7909  fiprc  7924  sbthlem2  7956  sbthlem4  7958  sbthlem5  7959  nneneq  8028  sdom1  8045  fineqvlem  8059  nfielex  8074  findcard  8084  findcard2  8085  elfiun  8219  marypha1lem  8222  oicl  8317  oif  8318  oion  8324  hartogslem1  8330  hartogs  8332  wemapso2  8341  card2on  8342  0wdom  8358  brwdom2  8361  inf3lem6  8413  cantnflem3  8471  cantnflem4  8472  wemapwe  8477  cnfcom  8480  tctr  8499  r1tr  8522  r1rankidb  8550  r1pw  8591  scottex  8631  scott0  8632  bnd2  8639  tskwe  8659  oncard  8669  cardlim  8681  harsdom  8704  en2eleq  8714  dfac8alem  8735  cardaleph  8795  iunfictbso  8820  infmap2  8923  ackbij1lem18  8942  cff  8953  cfsuc  8962  cff1  8963  cflim2  8968  cfss  8970  sdom2en01  9007  infpssrlem4  9011  fin23lem7  9021  fin23lem11  9022  isfin2-2  9024  fin23lem26  9030  fin23lem19  9041  fin23lem17  9043  isf34lem2  9078  isf34lem4  9082  fin1a2lem6  9110  fin1a2lem10  9114  fin1a2lem12  9116  itunifn  9122  hsmexlem1  9131  axcc2lem  9141  dcomex  9152  axdc3lem4  9158  ondomon  9264  konigthlem  9269  pwcfsdom  9284  cfpwsdom  9285  axpowndlem3  9300  canth4  9348  canthnumlem  9349  canthwelem  9351  canthwe  9352  canthp1lem2  9354  pwfseqlem4  9363  pwfseqlem5  9364  gchaleph  9372  gch2  9376  winainflem  9394  0tsk  9456  rankcf  9478  tskcard  9482  gruina  9519  grutsk  9523  tskmid  9541  indpi  9608  nqereu  9630  mulcanenq  9661  recmulnq  9665  archnq  9681  ltsopr  9733  1ne0sr  9796  0idsr  9797  00sr  9799  leid  10012  lelttric  10023  divcan3  10590  lemul1a  10756  nn1suc  10918  nn0n0n1ge2b  11236  xnn0xr  11245  xnn0nemnf  11251  nn0lt10b  11316  nn0ind-raph  11353  elnn1uz2  11641  indstr2  11643  uzsupss  11656  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  xrnemnf  11827  xrnepnf  11828  mnfltxr  11837  xnn0n0n1ge2b  11841  nn0pnfge0OLD  11844  xrlttri  11848  xrlttr  11849  xrleid  11859  qbtwnxr  11905  xmullem2  11967  xlemul1a  11990  xrub  12014  reltxrnmnf  12043  ixxun  12062  xnn0xrge0  12196  fztpval  12272  fseq1p1m1  12283  elfznelfzob  12440  ltweuz  12622  fzfi  12633  fsuppmapnn0fiubex  12654  ser0f  12716  0exp  12757  faclbnd4lem1  12942  bcn1  12962  hashnemnf  12994  hashv01gt1  12995  hashsnle1  13066  hashgt12el2  13071  hashmap  13082  hashpw  13083  hashf1  13098  fz1isolem  13102  hash2prb  13111  wrdlndm  13176  0wrd0  13186  wrdlen1  13198  ccatvalfn  13218  wrdl1exs1  13246  swrdlen  13275  swrdspsleq  13301  cats1un  13327  wrdind  13328  wrd2ind  13329  swrdccatin1  13334  repswsymballbi  13378  cshw1  13419  scshwfzeqfzo  13423  wrdl2exs2  13538  trclfvcotr  13598  relexp1g  13614  relexp0rel  13625  relexprelg  13626  sqr0lem  13829  sqrtsq  13858  mptfzshft  14352  fsumrev  14353  prodf1f  14463  fprodrev  14546  egt2lt3  14773  0dvds  14840  nn0o  14937  divalgmod  14967  flodddiv4  14975  bitsp1o  14993  gcddvds  15063  bezout  15098  lcmdvds  15159  rpdvds  15212  1nprm  15230  prmind2  15236  nnoddn2prmb  15356  pcpre1  15385  vdwapf  15514  vdwapid1  15517  ram0  15564  ramz  15567  prmolefac  15588  cshws0  15646  prmlem0  15650  strle1  15800  restsspw  15915  prdsdsfn  15948  imasdsfn  15997  imasaddfnlem  16011  imasvscafn  16020  xpscfv  16045  xpsfrnel  16046  isacs1i  16141  cidfn  16163  fnhomeqhomf  16174  comffn  16188  isoval  16248  sscres  16306  cofucl  16371  idffth  16416  ressffth  16421  catcoppccl  16581  estrchomfn  16598  funcestrcsetclem4  16606  funcestrcsetclem7  16609  equivestrcsetc  16615  funcsetcestrclem4  16621  funcsetcestrclem7  16624  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  yonedainv  16744  pospo  16796  lubfun  16803  glbfun  16816  joindmss  16830  meetdmss  16844  ipopos  16983  acsficl2d  16999  dirref  17058  mgm0  17078  mgmidcl  17088  mgmlrid  17089  sgrp0  17114  cntzssv  17584  symggrp  17643  symgid  17644  idresperm  17652  pmtrfmvdn0  17705  symggen  17713  psgnunilem1  17736  psgnprfval  17764  slwpgp  17851  frgpmhm  18001  frgpuptinv  18007  frgpup3lem  18013  gsumzoppg  18167  gsumcom2  18197  abv0  18654  rrgsupp  19112  psrvscafval  19211  psrridm  19225  ltbwe  19293  psrbag0  19315  psrbagsn  19316  subrgascl  19319  zrhrhm  19679  psgnodpmr  19755  frlmphl  19939  ellspd  19960  mattpostpos  20079  mavmul0  20177  mavmul0g  20178  mdet0f1o  20218  m1detdiag  20222  m2detleiblem5  20250  m2detleiblem6  20251  m2detleiblem3  20254  m2detleiblem4  20255  maducoeval2  20265  d1mat2pmat  20363  chpmat1dlem  20459  chpmat1d  20460  baspartn  20569  eltg3  20577  fctop  20618  cctop  20620  discld  20703  mretopd  20706  neipeltop  20743  neitr  20794  restcls  20795  ordtbaslem  20802  ordtuni  20804  idcn  20871  cnrmi  20974  cmpsublem  21012  cmpsub  21013  tgcmp  21014  uncmp  21016  hauscmplem  21019  cmpfi  21021  bwth  21023  1stcrestlem  21065  disllycmp  21111  dis1stc  21112  refref  21126  kgeni  21150  1stckgenlem  21166  kqffn  21338  snfil  21478  filcon  21497  cfinfil  21507  ufileu  21533  filufint  21534  fixufil  21536  cfinufil  21542  ufilen  21544  fin1aufil  21546  fmf  21559  rnelfm  21567  flimclslem  21598  hauspwpwf1  21601  supnfcls  21634  flimfnfcls  21642  fclscmp  21644  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALT  21665  ptcmplem1  21666  cnextrel  21677  tsmsfbas  21741  ustref  21832  trust  21843  restutop  21851  isusp  21875  xmet0  21957  imasdsf1olem  21988  blfvalps  21998  blfps  22021  blf  22022  restmetu  22185  dscmet  22187  isngp2  22211  nm0  22243  nrginvrcn  22306  nmoix  22343  qdensere  22383  iccconn  22441  iccpnfcnv  22551  xrhmeo  22553  lebnumlem3  22570  cmetss  22921  bcthlem5  22933  rrxmfval  22997  minveclem3b  23007  cniccbdd  23037  ovolicc2lem4  23095  iunmbl  23128  ioorinv  23150  ioorcl  23151  i1f1lem  23262  limcvallem  23441  ellimc2  23447  limccnp  23461  limccnp2  23462  limcco  23463  perfdvf  23473  recnprss  23474  fncpn  23502  dvcmulf  23514  c1lip1  23564  lhop2  23582  q1pcl  23719  r1pdeglt  23722  ply1remlem  23726  plyssc  23760  ulm0  23949  cxpeq0  24224  cxplea  24242  cxplogb  24324  asinlem  24395  isppw2  24641  muval2  24660  dchrfi  24780  dchrpt  24792  bposlem6  24814  lgsdir2lem2  24851  lgsqr  24876  gausslemma2dlem4  24894  2lgslem2  24920  2lgslem3  24929  2lgs  24932  2sqlem7  24949  2sqlem11  24954  chtppilim  24964  tgldimor  25197  tgcgr4  25226  tglnfn  25242  tglnunirn  25243  mirne  25362  mircinv  25363  perpln1  25405  perpln2  25406  lmiisolem  25488  xmstrkgc  25566  axcgrtr  25595  axsegconlem9  25605  axlowdimlem5  25626  axlowdimlem17  25638  axlowdim1  25639  uhgr0e  25737  uhgra0  25838  uhgra0v  25839  umgra0  25854  usgra0v  25900  usgraedg4  25916  usgra1v  25919  usgraexmpl  25930  nb3graprlem1  25980  cusgra1v  25990  cusgraexilem2  25996  uvtx01vtx  26020  wlkcomp  26053  wlkntrl  26092  0spth  26101  1pthonlem1  26119  2pthlem1  26125  usgra2wlkspthlem1  26147  3v3e3cycl1  26172  constr3trllem1  26178  constr3pthlem3  26185  4cycl4v4e  26194  4cycl4dv  26195  0conngra  26202  wwlkn0s  26233  clwlkcomp  26291  frgra0v  26520  frgra1v  26525  1vwmgra  26530  vdgfrgragt2  26554  frgrancvvdeqlem3  26559  frgrawopreg1  26577  frgrawopreg2  26578  2spot0  26591  ex-opab  26681  grpoinvf  26770  nvmid  26898  nmlnoubi  27035  hiidrcl  27336  hsn0elch  27489  shjshseli  27736  cmbr4i  27844  dfiop2  27996  kbpj  28199  nmopun  28257  adjeq0  28334  kbass2  28360  pjssdif1i  28418  pjinvari  28434  pjcmul2i  28445  pj3i  28451  stge1i  28481  stle0i  28482  sumdmdlem2  28662  dmdbr6ati  28666  dmdbr7ati  28667  rabsnel  28726  disjdifprg  28770  ofoprabco  28847  padct  28885  fpwrelmapffslem  28895  xrlelttric  28906  iundisj2cnt  28945  f1ocnt  28946  fz1nnct  28947  fz1nntr  28948  nn0min  28954  xrge0tsmsbi  29117  locfinref  29236  dispcmp  29254  pstmxmet  29268  xrge0iifcnv  29307  xrge0iif1  29312  qqhre  29392  esumcl  29419  esumpr2  29456  esumpinfval  29462  esumpcvgval  29467  ofcfn  29489  pwsiga  29520  prsiga  29521  sigainb  29526  ldgenpisyslem1  29553  measiuns  29607  relfae  29637  pmeasmono  29713  sitgf  29736  eulerpartgbij  29761  sgnmulsgn  29938  sgnmulsgp  29939  signswch  29964  signslema  29965  signstlen  29970  bnj145OLD  30049  bnj216  30054  bnj151  30201  bnj517  30209  bnj970  30271  bnj1145  30315  bnj1498  30383  subfacp1lem5  30420  erdszelem8  30434  kur14lem1  30442  indispcon  30470  cvmsss2  30510  msubrn  30680  dfpo2  30898  dfon2lem7  30938  frrlem6  31033  nosgnn0i  31056  nobndlem2  31092  nobndlem4  31094  nobndlem5  31095  nobndlem6  31096  brbigcup  31175  elsingles  31195  fnimage  31206  funpartlem  31219  dfrdg4  31228  imagesset  31230  altopthsn  31238  elaltxp  31252  ellines  31429  linethru  31430  rankeq1o  31448  elhf2  31452  hfninf  31463  nn0prpwlem  31487  fneref  31515  neibastop2lem  31525  limsucncmpi  31614  bj-speiv  31911  bj-exlimmpbir  32099  bj-snglex  32154  bj-restpw  32226  bj-topnex  32247  bj-inftyexpidisj  32274  topdifinffinlem  32371  relowlssretop  32387  rdgeqoa  32394  finxpreclem6  32409  poimirlem23  32602  poimirlem29  32608  poimirlem31  32610  volsupnfl  32624  cnambfre  32628  dvasin  32666  dvacos  32667  sdclem2  32708  sstotbnd2  32743  ssbnd  32757  ismgmOLD  32819  grpokerinj  32862  rngomndo  32904  isdrngo1  32925  ac6s6  33150  prtlem12  33170  riotasv2d  33261  lkrscss  33403  islshpkrN  33425  isline  34043  ispointN  34046  0psubN  34053  linepsubN  34056  atpsubN  34057  cdlemk36  35219  diafn  35341  dibfna  35461  dibvalrel  35470  dicvalrelN  35492  diclspsn  35501  dihvalrel  35586  dih1  35593  lclkrlem1  35813  lclkr  35840  mapd1o  35955  mapdin  35969  hdmapfnN  36139  hgmapfnN  36198  elrfirn  36276  ismrcd1  36279  istopclsd  36281  rabren3dioph  36397  jm2.17b  36546  jm2.22  36580  jm2.23  36581  ttac  36621  pw2f1ocnv  36622  dnnumch1  36632  hbtlem5  36717  mncn0  36728  aaitgo  36751  rngunsnply  36762  clcnvlem  36949  relexp01min  37024  ntrf  37441  ssrecnpr  37529  seff  37530  sblpnf  37531  nzss  37538  dvconstbi  37555  ipo0  37674  ifr0  37675  addrfn  37697  subrfn  37698  mulvfn  37699  refsum2cnlem1  38219  mapsnd  38383  ellimciota  38681  dvmptconst  38803  dvmptidg  38805  dvmulcncf  38815  dvdivcncf  38817  stoweidlem26  38919  stoweidlem50  38943  stoweidlem57  38950  iccpartiltu  39960  iccpartigtl  39961  zofldiv2ALTV  40112  evenprm2  40161  stgoldbwt  40198  nnsum3primesle9  40210  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  tgblthelfgott  40229  tgblthelfgottOLD  40236  funop1  40327  fun2dmnopgexmpl  40329  2ffzoeq  40361  uhgruhgra  40375  uhgr0edgfi  40466  issubgr2  40496  subgrprop2  40498  egrsubgr  40501  0grsubgr  40502  0uhgrsubgr  40503  uhgrsubgrself  40504  nbgr0vtx  40578  nbgr1vtx  40580  nb3grprlem1  40608  uvtxa0  40620  uvtxa01vtx0  40623  cplgr0v  40649  cplgr1vlem  40651  cplgr1v  40652  usgrexi  40661  1wlkcomp  40835  1wlk1walk  40843  1wlkp1lem5  40886  uhgr1wlkspthlem1  40959  pthdlem1  40972  clWlkcomp  40986  lfgrn1cycl  41008  uspgrn2crct  41011  wwlksn0s  41057  wwlksnonfi  41127  umgrwwlks2on  41161  0ewlk  41282  is01wlk  41285  is0Trl  41291  0spth-av  41294  upgr11wlkdlem2  41313  1wlk2v2e  41324  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  0vconngr  41360  frgr0v  41433  frgr1v  41441  1vwmgr  41446  frgrncvvdeqlem3  41471  frgrwopreg1  41487  frgrwopreg2  41488  0mgm  41564  nnsgrpmgm  41606  c0snmhm  41705  rngchomffvalALTV  41787  funcringcsetcALTV2lem4  41831  funcringcsetclem4ALTV  41854  srhmsubc  41868  rhmsubclem1  41878  srhmsubcALTV  41887  rhmsubcALTVlem1  41897  mapsnop  41916  zlmodzxzldeplem4  42086  zofldiv2  42119  fdivval  42131  nnlog2ge0lt1  42158  dig1  42200
  Copyright terms: Public domain W3C validator