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

Theorem mpbiri 261
 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 260 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  elimh  1080  spei  2401  nfald2  2456  nfabd2  2978  raleleqALT  3373  dedhb  3643  sbceqal  3782  csbie2df  4348  ssdifeq0  4390  r19.2zb  4399  dedth  4481  pwidg  4519  elpr2OLD  4551  snidg  4559  rexreusng  4577  exsnrex  4578  ifpr  4589  rmosn  4615  rabrsn  4620  prid1g  4656  tpid1g  4665  tpid2g  4667  tpid3g  4668  pwpw0  4706  sssn  4719  elpreqpr  4757  pwsnOLD  4793  unimax  4836  intmin3  4866  eqbrtrdi  5069  al0ssb  5176  intabs  5209  pwnss  5215  difelpw  5217  rabelpw  5218  0inp0  5224  copsexgw  5346  copsexg  5347  euotd  5368  elopab  5379  elvvuni  5592  posn  5601  frsn  5603  eqrelriv  5626  relsnb  5639  relopabiALT  5659  opabid2  5664  ididg  5688  iss  5870  ord0eln0  6213  sucidg  6237  nsuceq0  6239  onun2i  6274  funopg  6358  fn0  6451  f00  6535  f0bi  6536  f10d  6623  f1o00  6624  fo00  6625  brprcneu  6637  dffn5  6699  fsn  6874  funop  6888  funsndifnop  6890  fnsnb  6905  eufnfv  6969  f1eqcocnv  7035  f1eqcocnvOLD  7036  nfriotadw  7101  nfriotad  7104  riotaprop  7120  oprabidw  7166  oprabid  7167  elrnmpo  7266  ov6g  7292  ovelrn  7304  caovmo  7365  offn  7400  caofinvl  7416  fr3nr  7474  onprc  7479  ordeleqon  7483  onint0  7491  0elsuc  7530  onuninsuci  7535  orduninsuc  7538  ordzsl  7540  onzsl  7541  tfinds  7554  limomss  7565  limom  7575  peano5  7585  xpexr  7605  eqop2  7714  opreuopreu  7716  1stconst  7778  2ndconst  7779  funsssuppss  7839  dftpos3  7893  dftpos4  7894  wfrlem4  7941  wfrlem14  7951  oawordeulem  8163  omwordi  8180  nnmwordi  8244  riiner  8353  ecopover  8384  map0g  8431  mapsnd  8433  elixpsn  8484  en0  8555  en1  8559  fiprc  8578  sbthlem2  8612  sbthlem4  8614  sbthlem5  8615  nneneq  8684  sdom1  8702  fineqvlem  8716  nfielex  8731  findcard  8741  findcard2  8742  elfiun  8878  marypha1lem  8881  oicl  8977  oif  8978  oion  8984  hartogslem1  8990  hartogs  8992  wemapso2  9001  card2on  9002  0wdom  9018  brwdom2  9021  inf3lem6  9080  cantnflem3  9138  cantnflem4  9139  wemapwe  9144  cnfcom  9147  tctr  9166  r1tr  9189  r1rankidb  9217  r1pw  9258  scottex  9298  scott0  9299  bnd2  9306  eldju2ndl  9337  tskwe  9363  oncard  9373  cardlim  9385  harsdom  9408  en2eleq  9419  dfac8alem  9440  cardaleph  9500  iunfictbso  9525  infmap2  9629  ackbij1lem18  9648  cff  9659  cfsuc  9668  cff1  9669  cflim2  9674  cfss  9676  sdom2en01  9713  infpssrlem4  9717  fin23lem7  9727  fin23lem11  9728  isfin2-2  9730  fin23lem26  9736  fin23lem19  9747  fin23lem17  9749  isf34lem2  9784  isf34lem4  9788  fin1a2lem6  9816  fin1a2lem10  9820  fin1a2lem12  9822  itunifn  9828  hsmexlem1  9837  axcc2lem  9847  dcomex  9858  axdc3lem4  9864  ondomon  9974  konigthlem  9979  pwcfsdom  9994  cfpwsdom  9995  axpowndlem3  10010  canth4  10058  canthnumlem  10059  canthwelem  10061  canthwe  10062  canthp1lem2  10064  pwfseqlem4  10073  pwfseqlem5  10074  gchaleph  10082  gch2  10086  winainflem  10104  0tsk  10166  rankcf  10188  tskcard  10192  gruina  10229  grutsk  10233  tskmid  10251  indpi  10318  nqereu  10340  mulcanenq  10371  recmulnq  10375  archnq  10391  ltsopr  10443  1ne0sr  10507  0idsr  10508  00sr  10510  leid  10725  lelttric  10736  divcan3  11313  lemul1a  11483  nn1suc  11647  nn0n0n1ge2b  11951  xnn0xr  11960  xnn0nemnf  11966  nn0lt10b  12032  nn0ind-raph  12070  elnn1uz2  12313  indstr2  12315  uzsupss  12328  rpnnen1lem4  12367  rpnnen1lem5  12368  xrnemnf  12500  xrnepnf  12501  mnfltxr  12510  xnn0n0n1ge2b  12514  xnn0ge0  12516  xrlttri  12520  xrlttr  12521  xrleid  12532  qbtwnxr  12581  xmullem2  12646  xlemul1a  12669  xrub  12693  reltxrnmnf  12723  ixxun  12742  xnn0xrge0  12884  fztpval  12964  fseq1p1m1  12976  elfznelfzob  13138  ltweuz  13324  fzfi  13335  fsuppmapnn0fiubex  13355  ser0f  13419  0exp  13460  faclbnd4lem1  13649  bcn1  13669  hashnemnf  13700  hashv01gt1  13701  hashsnle1  13774  hashgt12el2  13780  hashpw  13793  hashf1  13811  fz1isolem  13815  hash2prb  13826  0wrd0  13883  wrdlen1  13897  ccatvalfn  13926  eqs1  13957  wrdl1exs1  13958  swrdlen  14000  swrdwrdsymb  14015  swrdspsleq  14018  cats1un  14074  wrdind  14075  wrd2ind  14076  swrdccatin1  14078  repswsymballbi  14133  cshw1  14175  scshwfzeqfzo  14179  wrdl2exs2  14299  trclfvcotr  14360  relexp1g  14377  relexp0rel  14388  relexprelg  14389  relexpreld  14391  sqr0lem  14592  sqrtsq  14621  mptfzshft  15125  prodf1f  15240  fprodrev  15323  egt2lt3  15551  0dvds  15622  nn0onn  15721  nn0o  15724  divalgmod  15747  flodddiv4  15754  bitsp1o  15772  gcddvds  15842  bezout  15881  lcmdvds  15942  rpdvds  15994  1nprm  16013  prmind2  16019  nnoddn2prmb  16140  pcpre1  16169  vdwapf  16298  vdwapid1  16301  ram0  16348  ramz  16351  prmolefac  16372  cshws0  16427  prmlem0  16431  strle1  16584  restsspw  16697  prdsdsfn  16730  imasdsfn  16779  imasaddfnlem  16793  imasvscafn  16802  xpsfrnel  16827  isacs1i  16920  cidfn  16942  fnhomeqhomf  16953  comffn  16967  isoval  17027  sscres  17085  cofucl  17150  idffth  17195  ressffth  17200  catcoppccl  17360  estrchomfn  17377  funcestrcsetclem4  17385  funcestrcsetclem7  17388  equivestrcsetc  17394  funcsetcestrclem4  17400  funcsetcestrclem7  17403  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  yonedainv  17523  pospo  17575  lubfun  17582  glbfun  17595  joindmss  17609  meetdmss  17623  ipopos  17762  acsficl2d  17778  dirref  17837  mgmidcl  17868  mgmlrid  17869  ielefmnd  18044  smndex1basss  18062  smndex1n0mnd  18069  cntzssv  18450  idresperm  18506  symgvalstruct  18517  pmtrfmvdn0  18582  symggen  18590  psgnunilem1  18613  psgnprfval  18641  slwpgp  18730  frgpmhm  18883  frgpuptinv  18889  frgpup3lem  18895  gsumzoppg  19057  gsumcom2  19088  abv0  19595  rrgsupp  20057  zrhrhm  20205  psgnodpmr  20279  frlmphllem  20469  frlmphl  20470  ellspd  20491  psrvscafval  20628  psrridm  20642  ltbwe  20712  psrbag0  20733  psrbagsn  20734  subrgascl  20737  mattpostpos  21059  mavmul0  21157  mavmul0g  21158  mdet0f1o  21198  m1detdiag  21202  m2detleiblem5  21230  m2detleiblem6  21231  m2detleiblem3  21234  m2detleiblem4  21235  maducoeval2  21245  d1mat2pmat  21344  chpmat1dlem  21440  chpmat1d  21441  baspartn  21559  eltg3  21567  topnex  21601  fctop  21609  cctop  21611  discld  21694  mretopd  21697  neipeltop  21734  neitr  21785  restcls  21786  ordtbaslem  21793  ordtuni  21795  idcn  21862  cnrmi  21965  cmpsublem  22004  cmpsub  22005  tgcmp  22006  uncmp  22008  hauscmplem  22011  cmpfi  22013  bwth  22015  1stcrestlem  22057  disllycmp  22103  dis1stc  22104  refref  22118  kgeni  22142  1stckgenlem  22158  kqffn  22330  snfil  22469  filconn  22488  cfinfil  22498  ufileu  22524  filufint  22525  fixufil  22527  cfinufil  22533  ufilen  22535  fin1aufil  22537  fmf  22550  rnelfm  22558  flimclslem  22589  hauspwpwf1  22592  supnfcls  22625  flimfnfcls  22633  fclscmp  22635  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALT  22656  ptcmplem1  22657  cnextrel  22668  tsmsfbas  22733  ustref  22824  trust  22835  restutop  22843  isusp  22867  xmet0  22949  imasdsf1olem  22980  blfvalps  22990  blfps  23013  blf  23014  restmetu  23177  dscmet  23179  isngp2  23203  nm0  23235  nrginvrcn  23298  nmoix  23335  qdensere  23375  iccconn  23435  iccpnfcnv  23549  xrhmeo  23551  lebnumlem3  23568  metsscmetcld  23919  bcthlem5  23932  csschl  23980  rrxmfval  24010  minveclem3b  24032  cniccbdd  24065  ovolicc2lem4  24124  iunmbl  24157  ioorinv  24180  ioorcl  24181  i1f1lem  24293  limcvallem  24474  ellimc2  24480  limccnp  24494  limccnp2  24495  limcco  24496  perfdvf  24506  recnprss  24507  fncpn  24536  dvcmulf  24548  c1lip1  24600  lhop2  24618  q1pcl  24756  r1pdeglt  24759  ply1remlem  24763  plyssc  24797  ulm0  24986  cxpeq0  25269  cxplea  25287  cxplogb  25372  asinlem  25454  isppw2  25700  muval2  25719  dchrfi  25839  dchrpt  25851  bposlem6  25873  lgsdir2lem2  25910  lgsqr  25935  gausslemma2dlem4  25953  2lgslem2  25979  2lgslem3  25988  2lgs  25991  2sqlem7  26008  2sqlem11  26013  chtppilim  26059  tgldimor  26296  tgcgr4  26325  tglnfn  26341  tglnunirn  26342  mirne  26461  mircinv  26462  perpln1  26504  perpln2  26505  lmiisolem  26590  xmstrkgc  26680  axcgrtr  26709  axsegconlem9  26719  axlowdimlem5  26740  axlowdimlem17  26752  axlowdim1  26753  uhgr0e  26864  edglnl  26936  uhgr0edgfi  27030  issubgr2  27062  subgrprop2  27064  egrsubgr  27067  0grsubgr  27068  0uhgrsubgr  27069  uhgrsubgrself  27070  nbgr0vtx  27146  nbgr1vtx  27148  nbgrssovtx  27151  nb3grprlem1  27170  uvtx01vtx  27187  cplgr1vlem  27219  cplgr1v  27220  usgrexilem  27230  wlkcomp  27420  wlk1walk  27428  wlkp1lem5  27467  uhgrwkspthlem1  27542  pthdlem1  27555  clwlkcomp  27568  lfgrn1cycl  27591  uspgrn2crct  27594  wwlksn0s  27647  umgrwwlks2on  27743  clwwlkn  27811  clwwlkn1  27826  0ewlk  27899  1ewlk  27900  0spth  27911  upgr1wlkdlem2  27931  wlk2v2e  27942  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eupth0  27999  frgr0v  28047  frgr1v  28056  1vwmgr  28061  ex-opab  28217  grpoinvf  28315  nvmid  28442  nmlnoubi  28579  hiidrcl  28878  hsn0elch  29031  shjshseli  29276  cmbr4i  29384  dfiop2  29536  kbpj  29739  nmopun  29797  adjeq0  29874  kbass2  29900  pjssdif1i  29958  pjinvari  29974  pjcmul2i  29985  pj3i  29991  stge1i  30021  stle0i  30022  sumdmdlem2  30202  dmdbr6ati  30206  dmdbr7ati  30207  rabsnel  30270  unidifsnel  30307  unidifsnne  30308  disjdifprg  30338  ofoprabco  30427  padct  30481  fpwrelmapffslem  30494  xrlelttric  30502  xnn0gt0  30520  iundisj2cnt  30548  f1ocnt  30551  fz1nnct  30552  fz1nntr  30553  hashxpe  30555  dvdszzq  30557  nn0min  30562  wrdt2ind  30653  xrge0tsmsbi  30743  locfinref  31194  dispcmp  31212  zartopn  31228  zarcmplem  31234  pstmxmet  31250  xrge0iifcnv  31286  xrge0iif1  31291  qqhre  31371  esumcl  31399  esumpr2  31436  esumpinfval  31442  esumpcvgval  31447  ofcfn  31469  pwsiga  31499  prsiga  31500  sigainb  31505  ldgenpisyslem1  31532  measiuns  31586  relfae  31616  pmeasmono  31692  sitgf  31715  eulerpartgbij  31740  sgnmulsgn  31917  sgnmulsgp  31918  signswch  31941  signslema  31942  signstlen  31947  signstfvn  31949  circlevma  32023  bnj216  32112  bnj151  32259  bnj517  32267  bnj970  32329  bnj1145  32375  bnj1498  32443  0nn0m1nnn0  32461  pthhashvtx  32484  acycgr0v  32505  prclisacycgr  32508  umgracycusgr  32511  cusgracyclt3v  32513  subfacp1lem5  32541  erdszelem8  32555  kur14lem1  32563  indispconn  32591  cvmsss2  32631  satfvsuclem2  32717  satfrel  32724  satfrnmapom  32727  satfv0fun  32728  satf00  32731  satf0suclem  32732  fmlasuc0  32741  msubrn  32886  dfpo2  33101  dfon2lem7  33144  nosgnn0i  33276  nolesgn2ores  33289  nosepnelem  33294  nosepdmlem  33297  nosupbnd1lem3  33320  nosupbnd1lem5  33322  nosupbnd2lem1  33325  brbigcup  33469  elsingles  33489  fnimage  33500  funpartlem  33513  dfrdg4  33522  imagesset  33524  altopthsn  33532  elaltxp  33546  ellines  33723  linethru  33724  rankeq1o  33742  elhf2  33746  hfninf  33757  nn0prpwlem  33780  fneref  33808  neibastop2lem  33818  limsucncmpi  33903  bj-exlimmpbir  34351  curryset  34378  bj-snglex  34406  bj-restpw  34504  bj-inftyexpidisj  34622  topdifinffinlem  34761  relowlssretop  34777  rdgeqoa  34784  finxpreclem6  34810  fvineqsneq  34826  pibt2  34831  poimirlem23  35077  poimirlem29  35083  poimirlem31  35085  volsupnfl  35099  cnambfre  35102  dvasin  35138  dvacos  35139  sdclem2  35177  sstotbnd2  35209  ssbnd  35223  ismgmOLD  35285  grpokerinj  35328  rngomndo  35370  isdrngo1  35391  ac6s6  35607  iss2  35758  cnvelrels  35892  cosselrels  35893  brssrid  35899  brcnvssrid  35904  dfdisjs5  36102  eldisjs5  36116  prtlem12  36160  riotasv2d  36250  lkrscss  36391  islshpkrN  36413  isline  37032  ispointN  37035  0psubN  37042  linepsubN  37045  atpsubN  37046  cdlemk36  38206  diafn  38327  dibfna  38447  dibvalrel  38456  dicvalrelN  38478  diclspsn  38487  dihvalrel  38572  dih1  38579  lclkrlem1  38799  lclkr  38826  mapd1o  38941  mapdin  38955  hdmapfnN  39122  hgmapfnN  39181  lcmineqlem10  39323  repncan2  39515  sn-inelr  39585  elrfirn  39631  ismrcd1  39634  istopclsd  39636  rabren3dioph  39751  jm2.17b  39897  jm2.22  39931  jm2.23  39932  ttac  39972  pw2f1ocnv  39973  dnnumch1  39983  hbtlem5  40067  mncn0  40078  aaitgo  40101  rngunsnply  40112  ensucne0OLD  40233  clcnvlem  40318  relexp01min  40409  ntrf  40821  ssrecnpr  41007  seff  41008  sblpnf  41009  nzss  41016  dvconstbi  41033  ipo0  41148  ifr0  41149  addrfn  41171  subrfn  41172  mulvfn  41173  refsum2cnlem1  41661  ellimciota  42251  dvmptconst  42552  dvmptidg  42554  dvmulcncf  42562  dvdivcncf  42564  stoweidlem26  42663  stoweidlem50  42687  stoweidlem57  42694  aiotaval  43645  ndfatafv2nrn  43772  afv2ndefb  43775  funop1  43834  fun2dmnopgexmpl  43835  2ffzoeq  43880  iccpartiltu  43934  iccpartigtl  43935  zofldiv2ALTV  44175  evenprm2  44227  9fppr8  44250  stgoldbwt  44289  nnsum3primesle9  44307  nnsum4primeseven  44313  nnsum4primesevenALTV  44314  tgblthelfgott  44328  isomgreqve  44338  uspgrex  44373  0mgm  44389  nnsgrpmgm  44431  c0snmhm  44534  rngchomffvalALTV  44614  funcringcsetcALTV2lem4  44658  funcringcsetclem4ALTV  44681  srhmsubc  44695  rhmsubclem1  44705  srhmsubcALTV  44713  rhmsubcALTVlem1  44723  mapsnop  44741  zlmodzxzldeplem4  44907  zofldiv2  44940  fdivval  44948  nnlog2ge0lt1  44975  dig1  45017  itcoval2  45073  itcoval3  45074
 Copyright terms: Public domain W3C validator