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

Theorem mpbiri 249
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 248 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  dedt  1097  spei  2437  nfald2  2495  nfabd2  2979  raleleqALT  3357  dedhb  3583  sbceqal  3696  ssdifeq0  4258  r19.2zb  4267  dedth  4346  pwidg  4377  elpr2  4405  snidg  4411  exsnrex  4425  ifpr  4436  rabrsn  4461  prid1g  4497  tpid3g  4507  pwpw0  4545  sssn  4558  elpreqpr  4600  pwsnALT  4634  unimax  4678  intmin3  4708  syl6eqbr  4894  al0ssb  4998  intabs  5030  pwnss  5035  0inp0  5042  copsexg  5158  euotd  5181  elopab  5191  epelg  5238  elvvuni  5393  posn  5403  frsn  5405  eqrelriv  5429  relopabiALT  5462  opabid2  5467  ididg  5491  iss  5666  ord0eln0  6005  sucidg  6029  nsuceq0  6031  onun2i  6066  funopg  6145  fn0  6232  f00  6312  f0bi  6313  f10d  6396  f1o00  6397  fo00  6398  brprcneu  6410  dffn5  6472  fsn  6635  funop  6648  funsndifnop  6650  funsneqopsnOLD  6651  fnsnb  6667  eufnfv  6726  f1eqcocnv  6790  nfriotad  6853  riotaprop  6869  oprabid  6915  elrnmpt2  7013  ov6g  7038  ovelrn  7050  caovmo  7111  offn  7148  caofinvl  7164  fr3nr  7219  onprc  7224  ordeleqon  7228  onint0  7236  0elsuc  7275  onuninsuci  7280  orduninsuc  7283  ordzsl  7285  onzsl  7286  tfinds  7299  limomss  7310  limom  7320  peano5  7329  xpexr  7346  eqop2  7451  1stconst  7509  2ndconst  7510  funsssuppss  7566  dftpos3  7615  dftpos4  7616  wfrlem4  7663  wfrlem4OLD  7664  wfrlem14  7674  oawordeulem  7881  omwordi  7898  nnmwordi  7962  riiner  8065  ecopover  8097  map0g  8143  mapsnd  8144  elixpsn  8194  en0  8265  en1  8269  fiprc  8288  sbthlem2  8320  sbthlem4  8322  sbthlem5  8323  nneneq  8392  sdom1  8409  fineqvlem  8423  nfielex  8438  findcard  8448  findcard2  8449  elfiun  8585  marypha1lem  8588  oicl  8683  oif  8684  oion  8690  hartogslem1  8696  hartogs  8698  wemapso2  8707  card2on  8708  0wdom  8724  brwdom2  8727  inf3lem6  8787  cantnflem3  8845  cantnflem4  8846  wemapwe  8851  cnfcom  8854  tctr  8873  r1tr  8896  r1rankidb  8924  r1pw  8965  scottex  9005  scott0  9006  bnd2  9013  eldju2ndl  9043  tskwe  9069  oncard  9079  cardlim  9091  harsdom  9114  en2eleq  9124  dfac8alem  9145  cardaleph  9205  iunfictbso  9230  infmap2  9335  ackbij1lem18  9354  cff  9365  cfsuc  9374  cff1  9375  cflim2  9380  cfss  9382  sdom2en01  9419  infpssrlem4  9423  fin23lem7  9433  fin23lem11  9434  isfin2-2  9436  fin23lem26  9442  fin23lem19  9453  fin23lem17  9455  isf34lem2  9490  isf34lem4  9494  fin1a2lem6  9522  fin1a2lem10  9526  fin1a2lem12  9528  itunifn  9534  hsmexlem1  9543  axcc2lem  9553  dcomex  9564  axdc3lem4  9570  ondomon  9680  konigthlem  9685  pwcfsdom  9700  cfpwsdom  9701  axpowndlem3  9716  canth4  9764  canthnumlem  9765  canthwelem  9767  canthwe  9768  canthp1lem2  9770  pwfseqlem4  9779  pwfseqlem5  9780  gchaleph  9788  gch2  9792  winainflem  9810  0tsk  9872  rankcf  9894  tskcard  9898  gruina  9935  grutsk  9939  tskmid  9957  indpi  10024  nqereu  10046  mulcanenq  10077  recmulnq  10081  archnq  10097  ltsopr  10149  1ne0sr  10212  0idsr  10213  00sr  10215  leid  10428  lelttric  10439  divcan3  11006  lemul1a  11172  nn1suc  11338  nn0n0n1ge2b  11645  xnn0xr  11654  xnn0nemnf  11660  nn0lt10b  11725  nn0ind-raph  11763  elnn1uz2  12004  indstr2  12006  uzsupss  12019  rpnnen1lem4  12056  rpnnen1lem5  12057  xrnemnf  12187  xrnepnf  12188  mnfltxr  12197  xnn0n0n1ge2b  12201  nn0pnfge0OLD  12204  xrlttri  12208  xrlttr  12209  xrleid  12220  qbtwnxr  12269  xmullem2  12333  xlemul1a  12356  xrub  12380  reltxrnmnf  12410  ixxun  12429  xnn0xrge0  12568  fztpval  12645  fseq1p1m1  12657  elfznelfzob  12818  ltweuz  13004  fzfi  13015  fsuppmapnn0fiubex  13035  ser0f  13097  0exp  13138  faclbnd4lem1  13320  bcn1  13340  hashnemnf  13372  hashv01gt1  13373  hashsnle1  13442  hashgt12el2  13448  hashpw  13460  hashf1  13478  fz1isolem  13482  hash2prb  13491  wrdlndm  13552  0wrd0  13562  wrdlen1  13575  ccatvalfn  13598  wrdl1exs1  13628  swrdlen  13666  swrdspsleq  13693  cats1un  13719  wrdind  13720  wrd2ind  13721  swrdccatin1  13727  repswsymballbi  13771  cshw1  13812  scshwfzeqfzo  13816  wrdl2exs2  13935  trclfvcotr  13993  relexp1g  14009  relexp0rel  14020  relexprelg  14021  sqr0lem  14224  sqrtsq  14253  mptfzshft  14752  fsumrev  14753  prodf1f  14865  fprodrev  14948  egt2lt3  15174  0dvds  15245  nn0o  15339  divalgmod  15369  flodddiv4  15376  bitsp1o  15394  gcddvds  15464  bezout  15499  lcmdvds  15560  rpdvds  15612  1nprm  15630  prmind2  15636  nnoddn2prmb  15755  pcpre1  15784  vdwapf  15913  vdwapid1  15916  ram0  15963  ramz  15966  prmolefac  15987  cshws0  16040  prmlem0  16044  strle1  16204  restsspw  16317  prdsdsfn  16350  imasdsfn  16399  imasaddfnlem  16413  imasvscafn  16422  xpscfv  16447  xpsfrnel  16448  isacs1i  16542  cidfn  16564  fnhomeqhomf  16575  comffn  16589  isoval  16649  sscres  16707  cofucl  16772  idffth  16817  ressffth  16822  catcoppccl  16982  estrchomfn  16999  funcestrcsetclem4  17008  funcestrcsetclem7  17011  equivestrcsetc  17017  funcsetcestrclem4  17023  funcsetcestrclem7  17026  1stfcl  17062  2ndfcl  17063  prfcl  17068  evlfcl  17087  curf1cl  17093  curfcl  17097  hofcl  17124  yonedainv  17146  pospo  17198  lubfun  17205  glbfun  17218  joindmss  17232  meetdmss  17246  ipopos  17385  acsficl2d  17401  dirref  17460  mgmidcl  17490  mgmlrid  17491  cntzssv  17982  symggrp  18041  symgid  18042  idresperm  18050  pmtrfmvdn0  18103  symggen  18111  psgnunilem1  18134  psgnprfval  18162  slwpgp  18249  frgpmhm  18399  frgpuptinv  18405  frgpup3lem  18411  gsumzoppg  18565  gsumcom2  18595  abv0  19055  rrgsupp  19520  psrvscafval  19619  psrridm  19633  ltbwe  19701  psrbag0  19722  psrbagsn  19723  subrgascl  19726  zrhrhm  20088  psgnodpmr  20163  frlmphl  20351  ellspd  20372  mattpostpos  20492  mavmul0  20590  mavmul0g  20591  mdet0f1o  20631  m1detdiag  20635  m2detleiblem5  20663  m2detleiblem6  20664  m2detleiblem3  20667  m2detleiblem4  20668  maducoeval2  20678  d1mat2pmat  20778  chpmat1dlem  20874  chpmat1d  20875  baspartn  20993  eltg3  21001  topnex  21035  fctop  21043  cctop  21045  discld  21128  mretopd  21131  neipeltop  21168  neitr  21219  restcls  21220  ordtbaslem  21227  ordtuni  21229  idcn  21296  cnrmi  21399  cmpsublem  21437  cmpsub  21438  tgcmp  21439  uncmp  21441  hauscmplem  21444  cmpfi  21446  bwth  21448  1stcrestlem  21490  disllycmp  21536  dis1stc  21537  refref  21551  kgeni  21575  1stckgenlem  21591  kqffn  21763  snfil  21902  filconn  21921  cfinfil  21931  ufileu  21957  filufint  21958  fixufil  21960  cfinufil  21966  ufilen  21968  fin1aufil  21970  fmf  21983  rnelfm  21991  flimclslem  22022  hauspwpwf1  22025  supnfcls  22058  flimfnfcls  22066  fclscmp  22068  alexsubALTlem2  22086  alexsubALTlem3  22087  alexsubALT  22089  ptcmplem1  22090  cnextrel  22101  tsmsfbas  22165  ustref  22256  trust  22267  restutop  22275  isusp  22299  xmet0  22381  imasdsf1olem  22412  blfvalps  22422  blfps  22445  blf  22446  restmetu  22609  dscmet  22611  isngp2  22635  nm0  22667  nrginvrcn  22730  nmoix  22767  qdensere  22807  iccconn  22867  iccpnfcnv  22977  xrhmeo  22979  lebnumlem3  22996  cmetss  23347  bcthlem5  23359  rrxmfval  23424  minveclem3b  23434  cniccbdd  23465  ovolicc2lem4  23524  iunmbl  23557  ioorinv  23580  ioorcl  23581  i1f1lem  23693  limcvallem  23872  ellimc2  23878  limccnp  23892  limccnp2  23893  limcco  23894  perfdvf  23904  recnprss  23905  fncpn  23933  dvcmulf  23945  c1lip1  23997  lhop2  24015  q1pcl  24152  r1pdeglt  24155  ply1remlem  24159  plyssc  24193  ulm0  24382  cxpeq0  24661  cxplea  24679  cxplogb  24761  asinlem  24832  isppw2  25078  muval2  25097  dchrfi  25217  dchrpt  25229  bposlem6  25251  lgsdir2lem2  25288  lgsqr  25313  gausslemma2dlem4  25331  2lgslem2  25357  2lgslem3  25366  2lgs  25369  2sqlem7  25386  2sqlem11  25391  chtppilim  25401  tgldimor  25634  tgcgr4  25663  tglnfn  25679  tglnunirn  25680  mirne  25799  mircinv  25800  perpln1  25842  perpln2  25843  lmiisolem  25925  xmstrkgc  26003  axcgrtr  26032  axsegconlem9  26042  axlowdimlem5  26063  axlowdimlem17  26075  axlowdim1  26076  uhgr0e  26203  edglnl  26276  uhgr0edgfi  26371  issubgr2  26403  subgrprop2  26405  egrsubgr  26408  0grsubgr  26409  0uhgrsubgr  26410  uhgrsubgrself  26411  nbgr0vtx  26491  nbgr1vtx  26493  nbgrssovtx  26496  nb3grprlem1  26521  uvtx01vtx  26541  uvtxa01vtx0OLD  26543  prcliscplgr  26560  cplgr1vlem  26576  cplgr1v  26577  usgrexilem  26587  wlkcomp  26777  wlk1walk  26786  wlkp1lem5  26825  uhgrwkspthlem1  26900  pthdlem1  26913  clwlkcomp  26926  lfgrn1cycl  26949  uspgrn2crct  26952  wwlksn0s  27011  umgrwwlks2on  27121  clwwlkn  27194  clwwlkn1  27213  0ewlk  27310  0spth  27322  upgr1wlkdlem2  27342  wlk2v2e  27353  upgr3v3e3cycl  27376  upgr4cycl4dv4e  27381  eupth0  27410  frgr0v  27459  frgr1v  27469  1vwmgr  27474  ex-opab  27643  grpoinvf  27738  nvmid  27865  nmlnoubi  28002  hiidrcl  28303  hsn0elch  28456  shjshseli  28703  cmbr4i  28811  dfiop2  28963  kbpj  29166  nmopun  29224  adjeq0  29301  kbass2  29327  pjssdif1i  29385  pjinvari  29401  pjcmul2i  29412  pj3i  29418  stge1i  29448  stle0i  29449  sumdmdlem2  29629  dmdbr6ati  29633  dmdbr7ati  29634  rabsnel  29689  disjdifprg  29736  ofoprabco  29814  padct  29847  fpwrelmapffslem  29857  xrlelttric  29867  iundisj2cnt  29908  f1ocnt  29909  fz1nnct  29910  fz1nntr  29911  nn0min  29917  xrge0tsmsbi  30134  locfinref  30256  dispcmp  30274  pstmxmet  30288  xrge0iifcnv  30327  xrge0iif1  30332  qqhre  30412  esumcl  30440  esumpr2  30477  esumpinfval  30483  esumpcvgval  30488  ofcfn  30510  pwsiga  30541  prsiga  30542  sigainb  30547  ldgenpisyslem1  30574  measiuns  30628  relfae  30658  pmeasmono  30734  sitgf  30757  eulerpartgbij  30782  sgnmulsgn  30959  sgnmulsgp  30960  signswch  30986  signslema  30987  signstlen  30992  circlevma  31068  bnj216  31146  bnj151  31292  bnj517  31300  bnj970  31362  bnj1145  31406  bnj1498  31474  subfacp1lem5  31511  erdszelem8  31525  kur14lem1  31533  indispconn  31561  cvmsss2  31601  msubrn  31771  dfpo2  31989  dfon2lem7  32036  nosgnn0i  32155  nolesgn2ores  32168  nosepnelem  32173  nosepdmlem  32176  nosupbnd1lem3  32199  nosupbnd1lem5  32201  nosupbnd2lem1  32204  brbigcup  32348  elsingles  32368  fnimage  32379  funpartlem  32392  dfrdg4  32401  imagesset  32403  altopthsn  32411  elaltxp  32425  ellines  32602  linethru  32603  rankeq1o  32621  elhf2  32625  hfninf  32636  nn0prpwlem  32660  fneref  32688  neibastop2lem  32698  limsucncmpi  32783  bj-speiv  33061  bj-exlimmpbir  33235  bj-snglex  33290  bj-restpw  33375  bj-inftyexpidisj  33433  topdifinffinlem  33530  relowlssretop  33546  rdgeqoa  33553  finxpreclem6  33568  cnfinltrel  33576  poimirlem23  33764  poimirlem29  33770  poimirlem31  33772  volsupnfl  33786  cnambfre  33789  dvasin  33827  dvacos  33828  sdclem2  33868  sstotbnd2  33903  ssbnd  33917  ismgmOLD  33979  grpokerinj  34022  rngomndo  34064  isdrngo1  34085  ac6s6  34309  iss2  34444  cnvelrels  34577  cosselrels  34578  brssrid  34584  brcnvssrid  34589  prtlem12  34665  riotasv2d  34755  lkrscss  34897  islshpkrN  34919  isline  35538  ispointN  35541  0psubN  35548  linepsubN  35551  atpsubN  35552  cdlemk36  36712  diafn  36833  dibfna  36953  dibvalrel  36962  dicvalrelN  36984  diclspsn  36993  dihvalrel  37078  dih1  37085  lclkrlem1  37305  lclkr  37332  mapd1o  37447  mapdin  37461  hdmapfnN  37628  hgmapfnN  37687  elrfirn  37778  ismrcd1  37781  istopclsd  37783  rabren3dioph  37899  jm2.17b  38047  jm2.22  38081  jm2.23  38082  ttac  38122  pw2f1ocnv  38123  dnnumch1  38133  hbtlem5  38217  mncn0  38228  aaitgo  38251  rngunsnply  38262  clcnvlem  38448  relexp01min  38523  ntrf  38939  ssrecnpr  39025  seff  39026  sblpnf  39027  nzss  39034  dvconstbi  39051  ipo0  39169  ifr0  39170  addrfn  39192  subrfn  39193  mulvfn  39194  refsum2cnlem1  39708  tpid2g  39825  tpid1g  39831  ellimciota  40344  dvmptconst  40627  dvmptidg  40629  dvmulcncf  40638  dvdivcncf  40640  stoweidlem26  40740  stoweidlem50  40764  stoweidlem57  40771  aiotaval  41695  ndfatafv2nrn  41828  afv2ndefb  41831  funop1  41891  fun2dmnopgexmpl  41892  2ffzoeq  41931  iccpartiltu  41951  iccpartigtl  41952  zofldiv2ALTV  42167  evenprm2  42216  stgoldbwt  42257  nnsum3primesle9  42275  nnsum4primeseven  42281  nnsum4primesevenALTV  42282  tgblthelfgott  42296  uspgrex  42344  0mgm  42360  nnsgrpmgm  42402  c0snmhm  42501  rngchomffvalALTV  42581  funcringcsetcALTV2lem4  42625  funcringcsetclem4ALTV  42648  srhmsubc  42662  rhmsubclem1  42672  srhmsubcALTV  42680  rhmsubcALTVlem1  42690  mapsnop  42709  zlmodzxzldeplem4  42878  zofldiv2  42911  fdivval  42919  nnlog2ge0lt1  42946  dig1  42988
  Copyright terms: Public domain W3C validator