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  1051  spei  2297  nfald2  2362  nfabd2  2813  raleleqALT  3187  dedhb  3409  sbceqal  3520  ssdifeq0  4084  r19.2zb  4094  dedth  4172  pwidg  4206  elpr2  4232  elpr2OLD  4233  snidg  4239  exsnrex  4253  ifpr  4265  rabrsn  4291  prid1g  4327  tpid3g  4337  pwpw0  4376  sssn  4390  elpreqpr  4427  pwsnALT  4461  unimax  4505  intmin3  4537  syl6eqbr  4724  intabs  4855  pwnss  4860  0inp0  4867  copsexg  4985  euotd  5004  elopab  5012  epelg  5059  elvvuni  5213  posn  5221  frsn  5223  eqrelriv  5247  relopabiALT  5279  opabid2  5284  ididg  5308  iss  5482  ord0eln0  5817  sucidg  5841  nsuceq0  5843  onun2i  5881  funopg  5960  fn0  6049  f00  6125  f0bi  6126  f10d  6208  f1o00  6209  fo00  6210  brprcneu  6222  dffn5  6280  fsn  6442  funop  6454  funsndifnop  6456  funsneqopsn  6457  fnsnb  6473  eufnfv  6531  f1eqcocnv  6596  nfriotad  6659  riotaprop  6675  oprabid  6717  elrnmpt2  6815  ov6g  6840  ovelrn  6852  caovmo  6913  offn  6950  caofinvl  6966  fr3nr  7021  onprc  7026  ordeleqon  7030  onint0  7038  0elsuc  7077  onuninsuci  7082  orduninsuc  7085  ordzsl  7087  onzsl  7088  tfinds  7101  limomss  7112  limom  7122  peano5  7131  xpexr  7148  eqop2  7253  1stconst  7310  2ndconst  7311  funsssuppss  7366  dftpos3  7415  dftpos4  7416  wfrlem4  7463  wfrlem14  7473  oawordeulem  7679  omwordi  7696  nnmwordi  7760  riiner  7863  ecopover  7894  map0g  7939  mapsn  7941  elixpsn  7989  en0  8060  en1  8064  fiprc  8080  sbthlem2  8112  sbthlem4  8114  sbthlem5  8115  nneneq  8184  sdom1  8201  fineqvlem  8215  nfielex  8230  findcard  8240  findcard2  8241  elfiun  8377  marypha1lem  8380  oicl  8475  oif  8476  oion  8482  hartogslem1  8488  hartogs  8490  wemapso2  8499  card2on  8500  0wdom  8516  brwdom2  8519  inf3lem6  8568  cantnflem3  8626  cantnflem4  8627  wemapwe  8632  cnfcom  8635  tctr  8654  r1tr  8677  r1rankidb  8705  r1pw  8746  scottex  8786  scott0  8787  bnd2  8794  tskwe  8814  oncard  8824  cardlim  8836  harsdom  8859  en2eleq  8869  dfac8alem  8890  cardaleph  8950  iunfictbso  8975  infmap2  9078  ackbij1lem18  9097  cff  9108  cfsuc  9117  cff1  9118  cflim2  9123  cfss  9125  sdom2en01  9162  infpssrlem4  9166  fin23lem7  9176  fin23lem11  9177  isfin2-2  9179  fin23lem26  9185  fin23lem19  9196  fin23lem17  9198  isf34lem2  9233  isf34lem4  9237  fin1a2lem6  9265  fin1a2lem10  9269  fin1a2lem12  9271  itunifn  9277  hsmexlem1  9286  axcc2lem  9296  dcomex  9307  axdc3lem4  9313  ondomon  9423  konigthlem  9428  pwcfsdom  9443  cfpwsdom  9444  axpowndlem3  9459  canth4  9507  canthnumlem  9508  canthwelem  9510  canthwe  9511  canthp1lem2  9513  pwfseqlem4  9522  pwfseqlem5  9523  gchaleph  9531  gch2  9535  winainflem  9553  0tsk  9615  rankcf  9637  tskcard  9641  gruina  9678  grutsk  9682  tskmid  9700  indpi  9767  nqereu  9789  mulcanenq  9820  recmulnq  9824  archnq  9840  ltsopr  9892  1ne0sr  9955  0idsr  9956  00sr  9958  leid  10171  lelttric  10182  divcan3  10749  lemul1a  10915  nn1suc  11079  nn0n0n1ge2b  11397  xnn0xr  11406  xnn0nemnf  11412  nn0lt10b  11477  nn0ind-raph  11515  elnn1uz2  11803  indstr2  11805  uzsupss  11818  rpnnen1lem4  11855  rpnnen1lem5  11856  rpnnen1lem4OLD  11861  rpnnen1lem5OLD  11862  xrnemnf  11989  xrnepnf  11990  mnfltxr  11999  xnn0n0n1ge2b  12003  nn0pnfge0OLD  12006  xrlttri  12010  xrlttr  12011  xrleid  12021  qbtwnxr  12069  xmullem2  12133  xlemul1a  12156  xrub  12180  reltxrnmnf  12210  ixxun  12229  xnn0xrge0  12363  fztpval  12440  fseq1p1m1  12452  elfznelfzob  12614  ltweuz  12800  fzfi  12811  fsuppmapnn0fiubex  12832  ser0f  12894  0exp  12935  faclbnd4lem1  13120  bcn1  13140  hashnemnf  13172  hashv01gt1  13173  hashsnle1  13243  hashgt12el2  13249  hashmap  13260  hashpw  13261  hashf1  13279  fz1isolem  13283  hash2prb  13292  wrdlndm  13353  0wrd0  13363  wrdlen1  13376  ccatvalfn  13399  wrdl1exs1  13430  swrdlen  13468  swrdspsleq  13495  cats1un  13521  wrdind  13522  wrd2ind  13523  swrdccatin1  13529  repswsymballbi  13573  cshw1  13614  scshwfzeqfzo  13618  wrdl2exs2  13736  trclfvcotr  13794  relexp1g  13810  relexp0rel  13821  relexprelg  13822  sqr0lem  14025  sqrtsq  14054  mptfzshft  14554  fsumrev  14555  prodf1f  14668  fprodrev  14751  egt2lt3  14978  0dvds  15049  nn0o  15146  divalgmod  15176  flodddiv4  15184  bitsp1o  15202  gcddvds  15272  bezout  15307  lcmdvds  15368  rpdvds  15421  1nprm  15439  prmind2  15445  nnoddn2prmb  15565  pcpre1  15594  vdwapf  15723  vdwapid1  15726  ram0  15773  ramz  15776  prmolefac  15797  cshws0  15855  prmlem0  15859  strle1  16020  restsspw  16139  prdsdsfn  16172  imasdsfn  16221  imasaddfnlem  16235  imasvscafn  16244  xpscfv  16269  xpsfrnel  16270  isacs1i  16365  cidfn  16387  fnhomeqhomf  16398  comffn  16412  isoval  16472  sscres  16530  cofucl  16595  idffth  16640  ressffth  16645  catcoppccl  16805  estrchomfn  16822  funcestrcsetclem4  16830  funcestrcsetclem7  16833  equivestrcsetc  16839  funcsetcestrclem4  16845  funcsetcestrclem7  16848  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  yonedainv  16968  pospo  17020  lubfun  17027  glbfun  17040  joindmss  17054  meetdmss  17068  ipopos  17207  acsficl2d  17223  dirref  17282  mgmidcl  17312  mgmlrid  17313  cntzssv  17807  symggrp  17866  symgid  17867  idresperm  17875  pmtrfmvdn0  17928  symggen  17936  psgnunilem1  17959  psgnprfval  17987  slwpgp  18074  frgpmhm  18224  frgpuptinv  18230  frgpup3lem  18236  gsumzoppg  18390  gsumcom2  18420  abv0  18879  rrgsupp  19339  psrvscafval  19438  psrridm  19452  ltbwe  19520  psrbag0  19542  psrbagsn  19543  subrgascl  19546  zrhrhm  19908  psgnodpmr  19984  frlmphl  20168  ellspd  20189  mattpostpos  20308  mavmul0  20406  mavmul0g  20407  mdet0f1o  20447  m1detdiag  20451  m2detleiblem5  20479  m2detleiblem6  20480  m2detleiblem3  20483  m2detleiblem4  20484  maducoeval2  20494  d1mat2pmat  20592  chpmat1dlem  20688  chpmat1d  20689  baspartn  20806  eltg3  20814  topnex  20848  fctop  20856  cctop  20858  discld  20941  mretopd  20944  neipeltop  20981  neitr  21032  restcls  21033  ordtbaslem  21040  ordtuni  21042  idcn  21109  cnrmi  21212  cmpsublem  21250  cmpsub  21251  tgcmp  21252  uncmp  21254  hauscmplem  21257  cmpfi  21259  bwth  21261  1stcrestlem  21303  disllycmp  21349  dis1stc  21350  refref  21364  kgeni  21388  1stckgenlem  21404  kqffn  21576  snfil  21715  filconn  21734  cfinfil  21744  ufileu  21770  filufint  21771  fixufil  21773  cfinufil  21779  ufilen  21781  fin1aufil  21783  fmf  21796  rnelfm  21804  flimclslem  21835  hauspwpwf1  21838  supnfcls  21871  flimfnfcls  21879  fclscmp  21881  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALT  21902  ptcmplem1  21903  cnextrel  21914  tsmsfbas  21978  ustref  22069  trust  22080  restutop  22088  isusp  22112  xmet0  22194  imasdsf1olem  22225  blfvalps  22235  blfps  22258  blf  22259  restmetu  22422  dscmet  22424  isngp2  22448  nm0  22480  nrginvrcn  22543  nmoix  22580  qdensere  22620  iccconn  22680  iccpnfcnv  22790  xrhmeo  22792  lebnumlem3  22809  cmetss  23159  bcthlem5  23171  rrxmfval  23235  minveclem3b  23245  cniccbdd  23276  ovolicc2lem4  23334  iunmbl  23367  ioorinv  23390  ioorcl  23391  i1f1lem  23501  limcvallem  23680  ellimc2  23686  limccnp  23700  limccnp2  23701  limcco  23702  perfdvf  23712  recnprss  23713  fncpn  23741  dvcmulf  23753  c1lip1  23805  lhop2  23823  q1pcl  23960  r1pdeglt  23963  ply1remlem  23967  plyssc  24001  ulm0  24190  cxpeq0  24469  cxplea  24487  cxplogb  24569  asinlem  24640  isppw2  24886  muval2  24905  dchrfi  25025  dchrpt  25037  bposlem6  25059  lgsdir2lem2  25096  lgsqr  25121  gausslemma2dlem4  25139  2lgslem2  25165  2lgslem3  25174  2lgs  25177  2sqlem7  25194  2sqlem11  25199  chtppilim  25209  tgldimor  25442  tgcgr4  25471  tglnfn  25487  tglnunirn  25488  mirne  25607  mircinv  25608  perpln1  25650  perpln2  25651  lmiisolem  25733  xmstrkgc  25811  axcgrtr  25840  axsegconlem9  25850  axlowdimlem5  25871  axlowdimlem17  25883  axlowdim1  25884  uhgr0e  26011  edglnl  26083  uhgr0edgfi  26177  issubgr2  26209  subgrprop2  26211  egrsubgr  26214  0grsubgr  26215  0uhgrsubgr  26216  uhgrsubgrself  26217  nbgr0vtx  26297  nbgr1vtx  26299  nbgrssovtx  26302  nb3grprlem1  26326  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  prcliscplgr  26365  cplgr1vlem  26381  cplgr1v  26382  usgrexilem  26392  wlkcomp  26582  wlk1walk  26591  wlkp1lem5  26630  uhgrwkspthlem1  26705  pthdlem1  26718  clwlkcomp  26731  lfgrn1cycl  26753  uspgrn2crct  26756  wwlksn0s  26815  umgrwwlks2on  26923  clwwlkn  26985  clwwlkn1  27004  0ewlk  27092  0spth  27104  upgr1wlkdlem2  27124  wlk2v2e  27135  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  eupth0  27192  frgr0v  27241  frgr1v  27251  1vwmgr  27256  ex-opab  27419  grpoinvf  27514  nvmid  27642  nmlnoubi  27779  hiidrcl  28080  hsn0elch  28233  shjshseli  28480  cmbr4i  28588  dfiop2  28740  kbpj  28943  nmopun  29001  adjeq0  29078  kbass2  29104  pjssdif1i  29162  pjinvari  29178  pjcmul2i  29189  pj3i  29195  stge1i  29225  stle0i  29226  sumdmdlem2  29406  dmdbr6ati  29410  dmdbr7ati  29411  rabsnel  29467  disjdifprg  29514  ofoprabco  29592  padct  29625  fpwrelmapffslem  29635  xrlelttric  29645  iundisj2cnt  29686  f1ocnt  29687  fz1nnct  29688  fz1nntr  29689  nn0min  29695  xrge0tsmsbi  29914  locfinref  30036  dispcmp  30054  pstmxmet  30068  xrge0iifcnv  30107  xrge0iif1  30112  qqhre  30192  esumcl  30220  esumpr2  30257  esumpinfval  30263  esumpcvgval  30268  ofcfn  30290  pwsiga  30321  prsiga  30322  sigainb  30327  ldgenpisyslem1  30354  measiuns  30408  relfae  30438  pmeasmono  30514  sitgf  30537  eulerpartgbij  30562  sgnmulsgn  30739  sgnmulsgp  30740  signswch  30766  signslema  30767  signstlen  30772  circlevma  30848  bnj216  30926  bnj151  31073  bnj517  31081  bnj970  31143  bnj1145  31187  bnj1498  31255  subfacp1lem5  31292  erdszelem8  31306  kur14lem1  31314  indispconn  31342  cvmsss2  31382  msubrn  31552  dfpo2  31771  dfon2lem7  31818  nosgnn0i  31937  nolesgn2ores  31950  nosepnelem  31955  nosepdmlem  31958  nosupbnd1lem3  31981  nosupbnd1lem5  31983  nosupbnd2lem1  31986  brbigcup  32130  elsingles  32150  fnimage  32161  funpartlem  32174  dfrdg4  32183  imagesset  32185  altopthsn  32193  elaltxp  32207  ellines  32384  linethru  32385  rankeq1o  32403  elhf2  32407  hfninf  32418  nn0prpwlem  32442  fneref  32470  neibastop2lem  32480  limsucncmpi  32569  bj-speiv  32849  bj-exlimmpbir  33032  bj-snglex  33086  bj-restpw  33170  bj-inftyexpidisj  33227  topdifinffinlem  33325  relowlssretop  33341  rdgeqoa  33348  finxpreclem6  33363  poimirlem23  33562  poimirlem29  33568  poimirlem31  33570  volsupnfl  33584  cnambfre  33588  dvasin  33626  dvacos  33627  sdclem2  33668  sstotbnd2  33703  ssbnd  33717  ismgmOLD  33779  grpokerinj  33822  rngomndo  33864  isdrngo1  33885  ac6s6  34110  iss2  34252  cnvelrels  34385  cosselrels  34386  brssrid  34392  brcnvssrid  34397  prtlem12  34471  riotasv2d  34561  lkrscss  34703  islshpkrN  34725  isline  35343  ispointN  35346  0psubN  35353  linepsubN  35356  atpsubN  35357  cdlemk36  36518  diafn  36640  dibfna  36760  dibvalrel  36769  dicvalrelN  36791  diclspsn  36800  dihvalrel  36885  dih1  36892  lclkrlem1  37112  lclkr  37139  mapd1o  37254  mapdin  37268  hdmapfnN  37438  hgmapfnN  37497  elrfirn  37575  ismrcd1  37578  istopclsd  37580  rabren3dioph  37696  jm2.17b  37845  jm2.22  37879  jm2.23  37880  ttac  37920  pw2f1ocnv  37921  dnnumch1  37931  hbtlem5  38015  mncn0  38026  aaitgo  38049  rngunsnply  38060  clcnvlem  38247  relexp01min  38322  ntrf  38738  ssrecnpr  38824  seff  38825  sblpnf  38826  nzss  38833  dvconstbi  38850  ipo0  38970  ifr0  38971  addrfn  38993  subrfn  38994  mulvfn  38995  refsum2cnlem1  39510  tpid2g  39630  tpid1g  39636  mapsnd  39702  ellimciota  40164  dvmptconst  40447  dvmptidg  40449  dvmulcncf  40458  dvdivcncf  40460  stoweidlem26  40561  stoweidlem50  40585  stoweidlem57  40592  funop1  41625  fun2dmnopgexmpl  41626  2ffzoeq  41663  iccpartiltu  41683  iccpartigtl  41684  zofldiv2ALTV  41899  evenprm2  41948  stgoldbwt  41989  nnsum3primesle9  42007  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  tgblthelfgott  42028  tgblthelfgottOLD  42034  uspgrex  42083  0mgm  42099  nnsgrpmgm  42141  c0snmhm  42240  rngchomffvalALTV  42320  funcringcsetcALTV2lem4  42364  funcringcsetclem4ALTV  42387  srhmsubc  42401  rhmsubclem1  42411  srhmsubcALTV  42419  rhmsubcALTVlem1  42429  mapsnop  42448  zlmodzxzldeplem4  42617  zofldiv2  42650  fdivval  42658  nnlog2ge0lt1  42685  dig1  42727
  Copyright terms: Public domain W3C validator