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

Theorem mpbiri 257
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 256 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  elimh  1083  spei  2392  nfald2  2443  nfabd2  2932  raleleqALT  3317  dedhb  3660  sbceqalOLD  3805  csbie2df  4399  ssdifeq0  4443  r19.2zb  4452  dedth  4543  pwidg  4579  elpr2OLD  4611  snidg  4619  rexreusng  4639  exsnrex  4640  ifpr  4651  rmosn  4679  rabrsn  4684  prid1g  4720  tpid1g  4729  tpid2g  4731  tpid3g  4732  pwpw0  4772  sssn  4785  elpreqpr  4823  pwsnOLD  4857  unimax  4904  intmin3  4936  eqbrtrdi  5143  al0ssb  5264  intabs  5298  pwnss  5305  difelpw  5307  rabelpw  5308  0inp0  5313  intidg  5413  copsexgw  5446  copsexg  5447  euotd  5469  elopab  5483  elvvuni  5707  posn  5716  frsn  5718  eqrelriv  5744  relsnb  5757  relopabiALT  5778  opabid2  5783  ididg  5808  iss  5988  dfpo2  6247  ord0eln0  6371  sucidg  6397  nsuceq0  6399  funopg  6533  fn0  6630  f00  6722  f0bi  6723  f10d  6816  f1o00  6817  fo00  6818  brprcneu  6830  brprcneuALT  6831  dffn5  6899  fsn  7078  funop  7092  funsndifnop  7094  fnsnb  7109  eufnfv  7176  f1eqcocnv  7244  f1eqcocnvOLD  7245  nfriotadw  7318  nfriotad  7322  riotaprop  7338  oprabidw  7385  oprabid  7386  elrnmpo  7489  ov6g  7515  ovelrn  7527  caovmo  7588  offn  7627  caofinvl  7644  fr3nr  7703  onprc  7709  ordeleqon  7713  onint0  7723  0elsuc  7767  onuninsuci  7773  orduninsuc  7776  ordzsl  7778  onzsl  7779  tfinds  7793  limomss  7804  limom  7815  peano5  7827  peano5OLD  7828  xpexr  7852  eqop2  7961  opreuopreu  7963  1stconst  8029  2ndconst  8030  frxp2  8073  frxp3  8080  funsssuppss  8118  dftpos3  8172  dftpos4  8173  wfrlem4OLD  8255  wfrlem14OLD  8265  oawordeulem  8498  omwordi  8515  nnmwordi  8579  riiner  8726  ecopover  8757  map0g  8819  mapsnd  8821  elixpsn  8872  en0  8954  en0OLD  8955  en0ALT  8956  en0r  8957  en1  8962  en1OLD  8963  fiprc  8986  sbthlem2  9025  sbthlem4  9027  sbthlem5  9028  0domg  9041  findcard  9104  findcard2  9105  nneneq  9150  nneneqOLD  9162  sdom1  9183  sdom1OLD  9184  1sdom2dom  9188  fineqvlem  9203  nfielex  9214  enp1i  9220  findcard2OLD  9225  elfiun  9363  marypha1lem  9366  oicl  9462  oif  9463  oion  9469  hartogslem1  9475  hartogs  9477  wemapso2  9486  card2on  9487  0wdom  9503  brwdom2  9506  inf3lem6  9566  cantnflem3  9624  cantnflem4  9625  wemapwe  9630  cnfcom  9633  ssttrcl  9648  ttrclselem2  9659  tctr  9673  r1tr  9709  r1rankidb  9737  r1pw  9778  scottex  9818  scott0  9819  bnd2  9826  eldju2ndl  9857  tskwe  9883  oncard  9893  cardlim  9905  harsdom  9928  en2eleq  9941  dfac8alem  9962  cardaleph  10022  iunfictbso  10047  infmap2  10151  ackbij1lem18  10170  cff  10181  cfsuc  10190  cff1  10191  cflim2  10196  cfss  10198  sdom2en01  10235  infpssrlem4  10239  fin23lem7  10249  fin23lem11  10250  isfin2-2  10252  fin23lem26  10258  fin23lem19  10269  fin23lem17  10271  isf34lem2  10306  isf34lem4  10310  fin1a2lem6  10338  fin1a2lem10  10342  fin1a2lem12  10344  itunifn  10350  hsmexlem1  10359  axcc2lem  10369  dcomex  10380  axdc3lem4  10386  ondomon  10496  konigthlem  10501  pwcfsdom  10516  cfpwsdom  10517  axpowndlem3  10532  canth4  10580  canthnumlem  10581  canthwelem  10583  canthwe  10584  canthp1lem2  10586  pwfseqlem4  10595  pwfseqlem5  10596  gchaleph  10604  gch2  10608  winainflem  10626  0tsk  10688  rankcf  10710  tskcard  10714  gruina  10751  grutsk  10755  tskmid  10773  indpi  10840  nqereu  10862  mulcanenq  10893  recmulnq  10897  archnq  10913  ltsopr  10965  1ne0sr  11029  0idsr  11030  00sr  11032  leid  11248  lelttric  11259  divcan3  11836  lemul1a  12006  nn1suc  12172  nn0n0n1ge2b  12478  xnn0xr  12487  xnn0nemnf  12493  nn0lt10b  12562  nn0ind-raph  12600  elnn1uz2  12847  indstr2  12849  uzsupss  12862  rpnnen1lem4  12902  rpnnen1lem5  12903  xrnemnf  13035  xrnepnf  13036  mnfltxr  13045  xnn0n0n1ge2b  13049  xnn0ge0  13051  xrlttri  13055  xrlttr  13056  xrleid  13067  qbtwnxr  13116  xmullem2  13181  xlemul1a  13204  xrub  13228  reltxrnmnf  13258  ixxun  13277  xnn0xrge0  13420  fztpval  13500  fseq1p1m1  13512  elfznelfzob  13675  ltweuz  13863  fzfi  13874  fsuppmapnn0fiubex  13894  ser0f  13958  0exp  14000  faclbnd4lem1  14190  bcn1  14210  hashnemnf  14241  hashv01gt1  14242  hashsnle1  14314  hashgt12el2  14320  hashpw  14333  hashf1  14353  fz1isolem  14357  hash2prb  14368  0wrd0  14425  wrdlen1  14439  ccatvalfn  14466  eqs1  14497  wrdl1exs1  14498  swrdlen  14532  swrdwrdsymb  14547  swrdspsleq  14550  cats1un  14606  wrdind  14607  wrd2ind  14608  swrdccatin1  14610  repswsymballbi  14665  cshw1  14707  scshwfzeqfzo  14712  wrdl2exs2  14832  trclfvcotr  14891  relexp1g  14908  relexp0rel  14919  relexprelg  14920  relexpreld  14922  sqrt0  15123  sqrtsq  15151  mptfzshft  15660  prodf1f  15774  egt2lt3  16085  0dvds  16156  nn0onn  16259  nn0o  16262  divalgmod  16285  flodddiv4  16292  bitsp1o  16310  gcddvds  16380  bezout  16421  lcmdvds  16481  rpdvds  16533  1nprm  16552  prmind2  16558  nnoddn2prmb  16682  pcpre1  16711  vdwapf  16841  vdwapid1  16844  ram0  16891  ramz  16894  prmolefac  16915  cshws0  16971  prmlem0  16975  strle1  17027  restsspw  17310  prdsdsfn  17344  imasdsfn  17393  imasaddfnlem  17407  imasvscafn  17416  xpsfrnel  17441  isacs1i  17534  cidfn  17556  fnhomeqhomf  17568  comffn  17582  isoval  17645  sscres  17703  cofucl  17771  idffth  17817  ressffth  17822  cat1lem  17979  catcoppccl  18000  catcoppcclOLD  18001  estrchomfn  18019  funcestrcsetclem4  18028  funcestrcsetclem7  18031  equivestrcsetc  18037  funcsetcestrclem4  18043  funcsetcestrclem7  18046  1stfcl  18082  2ndfcl  18083  prfcl  18088  evlfcl  18108  curf1cl  18114  curfcl  18118  hofcl  18145  yonedainv  18167  pospo  18231  lubfun  18238  glbfun  18251  joindmss  18265  meetdmss  18279  ipopos  18422  acsficl2d  18438  dirref  18487  mgmidcl  18518  mgmlrid  18519  ielefmnd  18694  smndex1basss  18712  smndex1n0mnd  18719  cntzssv  19104  idresperm  19163  symgvalstruct  19174  symgvalstructOLD  19175  pmtrfmvdn0  19240  symggen  19248  psgnunilem1  19271  psgnprfval  19299  slwpgp  19391  frgpmhm  19543  frgpuptinv  19549  frgpup3lem  19555  gsumzoppg  19717  gsumcom2  19748  abv0  20286  rrgsupp  20757  zrhrhm  20908  psgnodpmr  20990  frlmphllem  21182  frlmphl  21183  ellspd  21204  psrvscafval  21354  psrridm  21369  ltbwe  21441  psrbag0  21466  psrbagsn  21467  subrgascl  21470  mattpostpos  21799  mavmul0  21897  mavmul0g  21898  mdet0f1o  21938  m1detdiag  21942  m2detleiblem5  21970  m2detleiblem6  21971  m2detleiblem3  21974  m2detleiblem4  21975  maducoeval2  21985  d1mat2pmat  22084  chpmat1dlem  22180  chpmat1d  22181  baspartn  22300  eltg3  22308  topnex  22342  fctop  22350  cctop  22352  discld  22436  mretopd  22439  neipeltop  22476  neitr  22527  restcls  22528  ordtbaslem  22535  ordtuni  22537  idcn  22604  cnrmi  22707  cmpsublem  22746  cmpsub  22747  tgcmp  22748  uncmp  22750  hauscmplem  22753  cmpfi  22755  bwth  22757  1stcrestlem  22799  disllycmp  22845  dis1stc  22846  refref  22860  kgeni  22884  1stckgenlem  22900  kqffn  23072  snfil  23211  filconn  23230  cfinfil  23240  ufileu  23266  filufint  23267  fixufil  23269  cfinufil  23275  ufilen  23277  fin1aufil  23279  fmf  23292  rnelfm  23300  flimclslem  23331  hauspwpwf1  23334  supnfcls  23367  flimfnfcls  23375  fclscmp  23377  alexsubALTlem2  23395  alexsubALTlem3  23396  alexsubALT  23398  ptcmplem1  23399  cnextrel  23410  tsmsfbas  23475  ustref  23566  trust  23577  restutop  23585  isusp  23609  xmet0  23691  imasdsf1olem  23722  blfvalps  23732  blfps  23755  blf  23756  restmetu  23922  dscmet  23924  isngp2  23949  nm0  23981  nrginvrcn  24052  nmoix  24089  qdensere  24129  iccconn  24189  iccpnfcnv  24303  xrhmeo  24305  lebnumlem3  24322  metsscmetcld  24675  bcthlem5  24688  csschl  24736  rrxmfval  24766  minveclem3b  24788  cniccbdd  24821  ovolicc2lem4  24880  iunmbl  24913  ioorinv  24936  ioorcl  24937  i1f1lem  25049  limcvallem  25231  ellimc2  25237  limccnp  25251  limccnp2  25252  limcco  25253  perfdvf  25263  recnprss  25264  fncpn  25293  dvcmulf  25305  c1lip1  25357  lhop2  25375  q1pcl  25516  r1pdeglt  25519  ply1remlem  25523  plyssc  25557  ulm0  25746  cxpeq0  26029  cxplea  26047  cxplogb  26132  asinlem  26214  isppw2  26460  muval2  26479  dchrfi  26599  dchrpt  26611  bposlem6  26633  lgsdir2lem2  26670  lgsqr  26695  gausslemma2dlem4  26713  2lgslem2  26739  2lgslem3  26748  2lgs  26751  2sqlem7  26768  2sqlem11  26773  chtppilim  26819  nosgnn0i  27003  nolesgn2ores  27016  nogesgn1ores  27018  nosepnelem  27023  nosepdmlem  27027  nosupbnd1lem3  27054  nosupbnd1lem5  27056  nosupbnd2lem1  27059  noinfbnd1lem3  27069  noinfbnd1lem5  27071  noinfbnd2lem1  27074  oldval  27180  made0  27199  lrrecpo  27249  tgldimor  27342  tgcgr4  27371  tglnfn  27387  tglnunirn  27388  mirne  27507  mircinv  27508  perpln1  27550  perpln2  27551  lmiisolem  27636  xmstrkgc  27732  axcgrtr  27762  axsegconlem9  27772  axlowdimlem5  27793  axlowdimlem17  27805  axlowdim1  27806  uhgr0e  27920  edglnl  27992  uhgr0edgfi  28086  issubgr2  28118  subgrprop2  28120  egrsubgr  28123  0grsubgr  28124  0uhgrsubgr  28125  uhgrsubgrself  28126  nbgr0vtx  28202  nbgr1vtx  28204  nbgrssovtx  28207  nb3grprlem1  28226  uvtx01vtx  28243  cplgr1vlem  28275  cplgr1v  28276  usgrexilem  28286  wlkcomp  28477  wlk1walk  28485  wlkp1lem5  28523  uhgrwkspthlem1  28599  pthdlem1  28612  clwlkcomp  28625  lfgrn1cycl  28648  uspgrn2crct  28651  wwlksn0s  28704  umgrwwlks2on  28800  clwwlkn  28868  clwwlkn1  28883  0ewlk  28956  1ewlk  28957  0spth  28968  upgr1wlkdlem2  28988  wlk2v2e  28999  upgr3v3e3cycl  29022  upgr4cycl4dv4e  29027  eupth0  29056  frgr0v  29104  frgr1v  29113  1vwmgr  29118  ex-opab  29274  grpoinvf  29372  nvmid  29499  nmlnoubi  29636  hiidrcl  29935  hsn0elch  30088  shjshseli  30333  cmbr4i  30441  dfiop2  30593  kbpj  30796  nmopun  30854  adjeq0  30931  kbass2  30957  pjssdif1i  31015  pjinvari  31031  pjcmul2i  31042  pj3i  31048  stge1i  31078  stle0i  31079  sumdmdlem2  31259  dmdbr6ati  31263  dmdbr7ati  31264  rabsnel  31326  unidifsnel  31360  unidifsnne  31361  disjdifprg  31391  ofoprabco  31478  padct  31531  fpwrelmapffslem  31544  xrlelttric  31552  xnn0gt0  31569  iundisj2cnt  31597  f1ocnt  31600  fz1nnct  31601  fz1nntr  31602  hashxpe  31604  dvdszzq  31606  nn0min  31611  wrdt2ind  31702  xrge0tsmsbi  31795  locfinref  32313  dispcmp  32331  zartopn  32347  zarcmplem  32353  pstmxmet  32369  xrge0iifcnv  32405  xrge0iif1  32410  qqhre  32492  esumcl  32520  esumpr2  32557  esumpinfval  32563  esumpcvgval  32568  ofcfn  32590  pwsiga  32620  prsiga  32621  sigainb  32626  ldgenpisyslem1  32653  measiuns  32707  relfae  32737  pmeasmono  32815  sitgf  32838  eulerpartgbij  32863  sgnmulsgn  33040  sgnmulsgp  33041  signswch  33064  signslema  33065  signstlen  33070  signstfvn  33072  circlevma  33146  bnj216  33235  bnj151  33380  bnj517  33388  bnj970  33450  bnj1145  33496  bnj1498  33564  fineqvrep  33587  fineqvac  33589  0nn0m1nnn0  33594  pthhashvtx  33612  acycgr0v  33633  prclisacycgr  33636  umgracycusgr  33639  cusgracyclt3v  33641  subfacp1lem5  33669  erdszelem8  33683  kur14lem1  33691  indispconn  33719  cvmsss2  33759  satfvsuclem2  33845  satfrel  33852  satfrnmapom  33855  satfv0fun  33856  satf00  33859  satf0suclem  33860  fmlasuc0  33869  msubrn  34014  dfon2lem7  34256  brbigcup  34472  elsingles  34492  fnimage  34503  funpartlem  34516  dfrdg4  34525  imagesset  34527  altopthsn  34535  elaltxp  34549  ellines  34726  linethru  34727  rankeq1o  34745  elhf2  34749  hfninf  34760  nn0prpwlem  34783  fneref  34811  neibastop2lem  34821  limsucncmpi  34906  bj-exlimmpbir  35370  curryset  35406  bj-snglex  35433  bj-restpw  35552  bj-inftyexpidisj  35670  topdifinffinlem  35807  relowlssretop  35823  rdgeqoa  35830  finxpreclem6  35856  fvineqsneq  35872  pibt2  35877  poimirlem23  36090  poimirlem29  36096  poimirlem31  36098  volsupnfl  36112  cnambfre  36115  dvasin  36151  dvacos  36152  sdclem2  36190  sstotbnd2  36222  ssbnd  36236  ismgmOLD  36298  grpokerinj  36341  rngomndo  36383  isdrngo1  36404  ac6s6  36620  iss2  36794  cnvelrels  36946  cosselrels  36947  brssrid  36953  brcnvssrid  36958  dfdisjs5  37163  eldisjs5  37177  mpets2  37292  pets  37303  prtlem12  37318  riotasv2d  37408  lkrscss  37549  islshpkrN  37571  isline  38191  ispointN  38194  0psubN  38201  linepsubN  38204  atpsubN  38205  cdlemk36  39365  diafn  39486  dibfna  39606  dibvalrel  39615  dicvalrelN  39637  diclspsn  39646  dihvalrel  39731  dih1  39738  lclkrlem1  39958  lclkr  39985  mapd1o  40100  mapdin  40114  hdmapfnN  40281  hgmapfnN  40340  lcmineqlem10  40484  sticksstones9  40551  sn-iotalem  40631  repncan2  40827  sn-inelr  40910  elrfirn  40994  ismrcd1  40997  istopclsd  40999  rabren3dioph  41114  jm2.17b  41261  jm2.22  41295  jm2.23  41296  ttac  41336  pw2f1ocnv  41337  dnnumch1  41347  hbtlem5  41431  mncn0  41442  aaitgo  41465  rngunsnply  41476  unielss  41528  onexlimgt  41553  cantnfresb  41634  dflim5  41639  safesnsupfiss  41667  safesnsupfidom1o  41669  safesnsupfilb  41670  ensucne0OLD  41782  clcnvlem  41875  relexp01min  41965  ntrf  42375  ssrecnpr  42568  seff  42569  sblpnf  42570  nzss  42577  dvconstbi  42594  ipo0  42709  ifr0  42710  addrfn  42732  subrfn  42733  mulvfn  42734  refsum2cnlem1  43222  rn1st  43477  ellimciota  43825  dvmptconst  44126  dvmptidg  44128  dvmulcncf  44136  dvdivcncf  44138  stoweidlem26  44237  stoweidlem50  44261  stoweidlem57  44268  aiotaval  45297  ndfatafv2nrn  45423  afv2ndefb  45426  funop1  45485  fun2dmnopgexmpl  45486  2ffzoeq  45530  iccpartiltu  45584  iccpartigtl  45585  zofldiv2ALTV  45824  evenprm2  45876  9fppr8  45899  stgoldbwt  45938  nnsum3primesle9  45956  nnsum4primeseven  45962  nnsum4primesevenALTV  45963  tgblthelfgott  45977  isomgreqve  45987  uspgrex  46022  0mgm  46038  nnsgrpmgm  46080  c0snmhm  46183  rngchomffvalALTV  46263  funcringcsetcALTV2lem4  46307  funcringcsetclem4ALTV  46330  srhmsubc  46344  rhmsubclem1  46354  srhmsubcALTV  46362  rhmsubcALTVlem1  46372  mapsnop  46390  zlmodzxzldeplem4  46554  zofldiv2  46587  fdivval  46595  nnlog2ge0lt1  46622  dig1  46664  itcoval2  46720  itcoval3  46721  mosn  46867  mo0  46868  mof02  46875  mofeu  46884  f102g  46888  f1mo  46889  f1omo  46897  intubeu  46979  unilbeu  46980  functhinclem1  47031  fullthinc  47036  thincciso  47039  indthinc  47042  indthincALT  47043
  Copyright terms: Public domain W3C validator