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

Theorem mpbiri 248
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 247 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  dedt  1067  spei  2422  nfald2  2480  nfabd2  2932  raleleqALT  3305  dedhb  3526  sbceqal  3637  ssdifeq0  4191  r19.2zb  4200  dedth  4276  pwidg  4310  elpr2  4337  snidg  4343  exsnrex  4357  ifpr  4368  rabrsn  4393  prid1g  4429  tpid3g  4439  pwpw0  4477  sssn  4490  elpreqpr  4531  pwsnALT  4565  unimax  4607  intmin3  4637  syl6eqbr  4823  intabs  4953  pwnss  4958  0inp0  4965  copsexg  5083  euotd  5106  elopab  5116  epelg  5163  elvvuni  5319  posn  5327  frsn  5329  eqrelriv  5353  relopabiALT  5385  opabid2  5390  ididg  5414  iss  5588  ord0eln0  5922  sucidg  5946  nsuceq0  5948  onun2i  5986  funopg  6065  fn0  6151  f00  6227  f0bi  6228  f10d  6311  f1o00  6312  fo00  6313  brprcneu  6325  dffn5  6383  fsn  6544  funop  6556  funsndifnop  6558  funsneqopsnOLD  6559  fnsnb  6575  eufnfv  6633  f1eqcocnv  6698  nfriotad  6761  riotaprop  6777  oprabid  6821  elrnmpt2  6919  ov6g  6944  ovelrn  6956  caovmo  7017  offn  7054  caofinvl  7070  fr3nr  7125  onprc  7130  ordeleqon  7134  onint0  7142  0elsuc  7181  onuninsuci  7186  orduninsuc  7189  ordzsl  7191  onzsl  7192  tfinds  7205  limomss  7216  limom  7226  peano5  7235  xpexr  7252  eqop2  7357  1stconst  7415  2ndconst  7416  funsssuppss  7472  dftpos3  7521  dftpos4  7522  wfrlem4  7569  wfrlem4OLD  7570  wfrlem14  7580  oawordeulem  7787  omwordi  7804  nnmwordi  7868  riiner  7971  ecopover  8003  map0g  8049  mapsnd  8050  elixpsn  8100  en0  8171  en1  8175  fiprc  8194  sbthlem2  8226  sbthlem4  8228  sbthlem5  8229  nneneq  8298  sdom1  8315  fineqvlem  8329  nfielex  8344  findcard  8354  findcard2  8355  elfiun  8491  marypha1lem  8494  oicl  8589  oif  8590  oion  8596  hartogslem1  8602  hartogs  8604  wemapso2  8613  card2on  8614  0wdom  8630  brwdom2  8633  inf3lem6  8693  cantnflem3  8751  cantnflem4  8752  wemapwe  8757  cnfcom  8760  tctr  8779  r1tr  8802  r1rankidb  8830  r1pw  8871  scottex  8911  scott0  8912  bnd2  8919  eldju2ndl  8949  tskwe  8975  oncard  8985  cardlim  8997  harsdom  9020  en2eleq  9030  dfac8alem  9051  cardaleph  9111  iunfictbso  9136  infmap2  9241  ackbij1lem18  9260  cff  9271  cfsuc  9280  cff1  9281  cflim2  9286  cfss  9288  sdom2en01  9325  infpssrlem4  9329  fin23lem7  9339  fin23lem11  9340  isfin2-2  9342  fin23lem26  9348  fin23lem19  9359  fin23lem17  9361  isf34lem2  9396  isf34lem4  9400  fin1a2lem6  9428  fin1a2lem10  9432  fin1a2lem12  9434  itunifn  9440  hsmexlem1  9449  axcc2lem  9459  dcomex  9470  axdc3lem4  9476  ondomon  9586  konigthlem  9591  pwcfsdom  9606  cfpwsdom  9607  axpowndlem3  9622  canth4  9670  canthnumlem  9671  canthwelem  9673  canthwe  9674  canthp1lem2  9676  pwfseqlem4  9685  pwfseqlem5  9686  gchaleph  9694  gch2  9698  winainflem  9716  0tsk  9778  rankcf  9800  tskcard  9804  gruina  9841  grutsk  9845  tskmid  9863  indpi  9930  nqereu  9952  mulcanenq  9983  recmulnq  9987  archnq  10003  ltsopr  10055  1ne0sr  10118  0idsr  10119  00sr  10121  leid  10334  lelttric  10345  divcan3  10912  lemul1a  11078  nn1suc  11242  nn0n0n1ge2b  11560  xnn0xr  11569  xnn0nemnf  11575  nn0lt10b  11640  nn0ind-raph  11678  elnn1uz2  11967  indstr2  11969  uzsupss  11982  rpnnen1lem4  12019  rpnnen1lem5  12020  rpnnen1lem4OLD  12025  rpnnen1lem5OLD  12026  xrnemnf  12155  xrnepnf  12156  mnfltxr  12165  xnn0n0n1ge2b  12169  nn0pnfge0OLD  12172  xrlttri  12176  xrlttr  12177  xrleid  12187  qbtwnxr  12235  xmullem2  12299  xlemul1a  12322  xrub  12346  reltxrnmnf  12376  ixxun  12395  xnn0xrge0  12531  fztpval  12608  fseq1p1m1  12620  elfznelfzob  12781  ltweuz  12967  fzfi  12978  fsuppmapnn0fiubex  12998  ser0f  13060  0exp  13101  faclbnd4lem1  13283  bcn1  13303  hashnemnf  13335  hashv01gt1  13336  hashsnle1  13406  hashgt12el2  13412  hashpw  13424  hashf1  13442  fz1isolem  13446  hash2prb  13455  wrdlndm  13516  0wrd0  13526  wrdlen1  13539  ccatvalfn  13562  wrdl1exs1  13592  swrdlen  13630  swrdspsleq  13657  cats1un  13683  wrdind  13684  wrd2ind  13685  swrdccatin1  13691  repswsymballbi  13735  cshw1  13776  scshwfzeqfzo  13780  wrdl2exs2  13899  trclfvcotr  13957  relexp1g  13973  relexp0rel  13984  relexprelg  13985  sqr0lem  14188  sqrtsq  14217  mptfzshft  14716  fsumrev  14717  prodf1f  14830  fprodrev  14913  egt2lt3  15139  0dvds  15210  nn0o  15306  divalgmod  15336  flodddiv4  15344  bitsp1o  15362  gcddvds  15432  bezout  15467  lcmdvds  15528  rpdvds  15580  1nprm  15598  prmind2  15604  nnoddn2prmb  15724  pcpre1  15753  vdwapf  15882  vdwapid1  15885  ram0  15932  ramz  15935  prmolefac  15956  cshws0  16014  prmlem0  16018  strle1  16180  restsspw  16299  prdsdsfn  16332  imasdsfn  16381  imasaddfnlem  16395  imasvscafn  16404  xpscfv  16429  xpsfrnel  16430  isacs1i  16524  cidfn  16546  fnhomeqhomf  16557  comffn  16571  isoval  16631  sscres  16689  cofucl  16754  idffth  16799  ressffth  16804  catcoppccl  16964  estrchomfn  16981  funcestrcsetclem4  16990  funcestrcsetclem7  16993  equivestrcsetc  16999  funcsetcestrclem4  17005  funcsetcestrclem7  17008  1stfcl  17044  2ndfcl  17045  prfcl  17050  evlfcl  17069  curf1cl  17075  curfcl  17079  hofcl  17106  yonedainv  17128  pospo  17180  lubfun  17187  glbfun  17200  joindmss  17214  meetdmss  17228  ipopos  17367  acsficl2d  17383  dirref  17442  mgmidcl  17472  mgmlrid  17473  cntzssv  17967  symggrp  18026  symgid  18027  idresperm  18035  pmtrfmvdn0  18088  symggen  18096  psgnunilem1  18119  psgnprfval  18147  slwpgp  18234  frgpmhm  18384  frgpuptinv  18390  frgpup3lem  18396  gsumzoppg  18550  gsumcom2  18580  abv0  19040  rrgsupp  19505  psrvscafval  19604  psrridm  19618  ltbwe  19686  psrbag0  19708  psrbagsn  19709  subrgascl  19712  zrhrhm  20074  psgnodpmr  20150  frlmphl  20336  ellspd  20357  mattpostpos  20477  mavmul0  20575  mavmul0g  20576  mdet0f1o  20616  m1detdiag  20620  m2detleiblem5  20648  m2detleiblem6  20649  m2detleiblem3  20652  m2detleiblem4  20653  maducoeval2  20663  d1mat2pmat  20763  chpmat1dlem  20859  chpmat1d  20860  baspartn  20978  eltg3  20986  topnex  21020  fctop  21028  cctop  21030  discld  21113  mretopd  21116  neipeltop  21153  neitr  21204  restcls  21205  ordtbaslem  21212  ordtuni  21214  idcn  21281  cnrmi  21384  cmpsublem  21422  cmpsub  21423  tgcmp  21424  uncmp  21426  hauscmplem  21429  cmpfi  21431  bwth  21433  1stcrestlem  21475  disllycmp  21521  dis1stc  21522  refref  21536  kgeni  21560  1stckgenlem  21576  kqffn  21748  snfil  21887  filconn  21906  cfinfil  21916  ufileu  21942  filufint  21943  fixufil  21945  cfinufil  21951  ufilen  21953  fin1aufil  21955  fmf  21968  rnelfm  21976  flimclslem  22007  hauspwpwf1  22010  supnfcls  22043  flimfnfcls  22051  fclscmp  22053  alexsubALTlem2  22071  alexsubALTlem3  22072  alexsubALT  22074  ptcmplem1  22075  cnextrel  22086  tsmsfbas  22150  ustref  22241  trust  22252  restutop  22260  isusp  22284  xmet0  22366  imasdsf1olem  22397  blfvalps  22407  blfps  22430  blf  22431  restmetu  22594  dscmet  22596  isngp2  22620  nm0  22652  nrginvrcn  22715  nmoix  22752  qdensere  22792  iccconn  22852  iccpnfcnv  22962  xrhmeo  22964  lebnumlem3  22981  cmetss  23331  bcthlem5  23343  rrxmfval  23407  minveclem3b  23417  cniccbdd  23448  ovolicc2lem4  23507  iunmbl  23540  ioorinv  23563  ioorcl  23564  i1f1lem  23675  limcvallem  23854  ellimc2  23860  limccnp  23874  limccnp2  23875  limcco  23876  perfdvf  23886  recnprss  23887  fncpn  23915  dvcmulf  23927  c1lip1  23979  lhop2  23997  q1pcl  24134  r1pdeglt  24137  ply1remlem  24141  plyssc  24175  ulm0  24364  cxpeq0  24644  cxplea  24662  cxplogb  24744  asinlem  24815  isppw2  25061  muval2  25080  dchrfi  25200  dchrpt  25212  bposlem6  25234  lgsdir2lem2  25271  lgsqr  25296  gausslemma2dlem4  25314  2lgslem2  25340  2lgslem3  25349  2lgs  25352  2sqlem7  25369  2sqlem11  25374  chtppilim  25384  tgldimor  25617  tgcgr4  25646  tglnfn  25662  tglnunirn  25663  mirne  25782  mircinv  25783  perpln1  25825  perpln2  25826  lmiisolem  25908  xmstrkgc  25986  axcgrtr  26015  axsegconlem9  26025  axlowdimlem5  26046  axlowdimlem17  26058  axlowdim1  26059  uhgr0e  26186  edglnl  26259  uhgr0edgfi  26354  issubgr2  26386  subgrprop2  26388  egrsubgr  26391  0grsubgr  26392  0uhgrsubgr  26393  uhgrsubgrself  26394  nbgr0vtx  26474  nbgr1vtx  26476  nbgrssovtx  26479  nb3grprlem1  26504  uvtx01vtx  26524  uvtxa01vtx0OLD  26526  prcliscplgr  26543  cplgr1vlem  26559  cplgr1v  26560  usgrexilem  26570  wlkcomp  26760  wlk1walk  26769  wlkp1lem5  26808  uhgrwkspthlem1  26883  pthdlem1  26896  clwlkcomp  26909  lfgrn1cycl  26932  uspgrn2crct  26935  wwlksn0s  26994  umgrwwlks2on  27102  clwwlkn  27175  clwwlkn1  27194  0ewlk  27291  0spth  27303  upgr1wlkdlem2  27323  wlk2v2e  27334  upgr3v3e3cycl  27357  upgr4cycl4dv4e  27362  eupth0  27391  frgr0v  27440  frgr1v  27450  1vwmgr  27455  ex-opab  27625  grpoinvf  27720  nvmid  27848  nmlnoubi  27985  hiidrcl  28286  hsn0elch  28439  shjshseli  28686  cmbr4i  28794  dfiop2  28946  kbpj  29149  nmopun  29207  adjeq0  29284  kbass2  29310  pjssdif1i  29368  pjinvari  29384  pjcmul2i  29395  pj3i  29401  stge1i  29431  stle0i  29432  sumdmdlem2  29612  dmdbr6ati  29616  dmdbr7ati  29617  rabsnel  29673  disjdifprg  29720  ofoprabco  29798  padct  29831  fpwrelmapffslem  29841  xrlelttric  29851  iundisj2cnt  29892  f1ocnt  29893  fz1nnct  29894  fz1nntr  29895  nn0min  29901  xrge0tsmsbi  30120  locfinref  30242  dispcmp  30260  pstmxmet  30274  xrge0iifcnv  30313  xrge0iif1  30318  qqhre  30398  esumcl  30426  esumpr2  30463  esumpinfval  30469  esumpcvgval  30474  ofcfn  30496  pwsiga  30527  prsiga  30528  sigainb  30533  ldgenpisyslem1  30560  measiuns  30614  relfae  30644  pmeasmono  30720  sitgf  30743  eulerpartgbij  30768  sgnmulsgn  30945  sgnmulsgp  30946  signswch  30972  signslema  30973  signstlen  30978  circlevma  31054  bnj216  31132  bnj151  31279  bnj517  31287  bnj970  31349  bnj1145  31393  bnj1498  31461  subfacp1lem5  31498  erdszelem8  31512  kur14lem1  31520  indispconn  31548  cvmsss2  31588  msubrn  31758  dfpo2  31977  dfon2lem7  32024  nosgnn0i  32143  nolesgn2ores  32156  nosepnelem  32161  nosepdmlem  32164  nosupbnd1lem3  32187  nosupbnd1lem5  32189  nosupbnd2lem1  32192  brbigcup  32336  elsingles  32356  fnimage  32367  funpartlem  32380  dfrdg4  32389  imagesset  32391  altopthsn  32399  elaltxp  32413  ellines  32590  linethru  32591  rankeq1o  32609  elhf2  32613  hfninf  32624  nn0prpwlem  32648  fneref  32676  neibastop2lem  32686  limsucncmpi  32775  bj-speiv  33055  bj-exlimmpbir  33231  bj-snglex  33286  bj-restpw  33370  bj-inftyexpidisj  33427  topdifinffinlem  33525  relowlssretop  33541  rdgeqoa  33548  finxpreclem6  33563  cnfinltrel  33571  poimirlem23  33758  poimirlem29  33764  poimirlem31  33766  volsupnfl  33780  cnambfre  33783  dvasin  33821  dvacos  33822  sdclem2  33863  sstotbnd2  33898  ssbnd  33912  ismgmOLD  33974  grpokerinj  34017  rngomndo  34059  isdrngo1  34080  ac6s6  34305  iss2  34447  cnvelrels  34580  cosselrels  34581  brssrid  34587  brcnvssrid  34592  prtlem12  34668  riotasv2d  34758  lkrscss  34900  islshpkrN  34922  isline  35540  ispointN  35543  0psubN  35550  linepsubN  35553  atpsubN  35554  cdlemk36  36715  diafn  36837  dibfna  36957  dibvalrel  36966  dicvalrelN  36988  diclspsn  36997  dihvalrel  37082  dih1  37089  lclkrlem1  37309  lclkr  37336  mapd1o  37451  mapdin  37465  hdmapfnN  37632  hgmapfnN  37691  elrfirn  37777  ismrcd1  37780  istopclsd  37782  rabren3dioph  37898  jm2.17b  38047  jm2.22  38081  jm2.23  38082  ttac  38122  pw2f1ocnv  38123  dnnumch1  38133  hbtlem5  38217  mncn0  38228  aaitgo  38251  rngunsnply  38262  clcnvlem  38449  relexp01min  38524  ntrf  38940  ssrecnpr  39026  seff  39027  sblpnf  39028  nzss  39035  dvconstbi  39052  ipo0  39172  ifr0  39173  addrfn  39195  subrfn  39196  mulvfn  39197  refsum2cnlem1  39712  tpid2g  39831  tpid1g  39837  ellimciota  40358  dvmptconst  40641  dvmptidg  40643  dvmulcncf  40652  dvdivcncf  40654  stoweidlem26  40754  stoweidlem50  40778  stoweidlem57  40785  funop1  41818  fun2dmnopgexmpl  41819  2ffzoeq  41856  iccpartiltu  41876  iccpartigtl  41877  zofldiv2ALTV  42092  evenprm2  42141  stgoldbwt  42182  nnsum3primesle9  42200  nnsum4primeseven  42206  nnsum4primesevenALTV  42207  tgblthelfgott  42221  tgblthelfgottOLD  42227  uspgrex  42276  0mgm  42292  nnsgrpmgm  42334  c0snmhm  42433  rngchomffvalALTV  42513  funcringcsetcALTV2lem4  42557  funcringcsetclem4ALTV  42580  srhmsubc  42594  rhmsubclem1  42604  srhmsubcALTV  42612  rhmsubcALTVlem1  42622  mapsnop  42641  zlmodzxzldeplem4  42810  zofldiv2  42843  fdivval  42851  nnlog2ge0lt1  42878  dig1  42920
  Copyright terms: Public domain W3C validator