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

Theorem mpbiri 233
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  |-  ch
mpbiri.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mpbiri  |-  ( ph  ->  ps )

Proof of Theorem mpbiri
StepHypRef Expression
1 mpbiri.min . . 3  |-  ch
21a1i 11 . 2  |-  ( ph  ->  ch )
3 mpbiri.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbird 232 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  dedt  948  spei  1956  nfald2  2023  nfabd2  2592  dedhb  3124  sbceqal  3237  sbcel12  3670  ssdifeq0  3756  r19.2zb  3765  dedth  3836  pwidg  3868  elpr2  3891  snidg  3898  exsnrex  3909  ifpr  3919  rabrsn  3940  prid1g  3976  pwpw0  4016  sssn  4026  preqr1  4041  pwsnALT  4081  unimax  4122  intmin3  4151  syl6eqbr  4324  intabs  4448  pwnss  4452  0inp0  4459  copsexg  4571  copsexgOLD  4572  euotd  4587  elopab  4592  epelg  4628  ord0eln0  4768  sucidg  4792  nsuceq0  4794  onun2i  4829  elvvuni  4894  posn  4902  frsn  4904  eqrelriv  4928  relopabi  4960  opabid2  4964  ididg  4988  iss  5149  funopg  5445  fn0  5525  f00  5588  f0bi  5589  f1o00  5668  fo00  5669  brprcneu  5679  dffn5  5732  fsn  5876  fnsnb  5893  fconstfv  5935  eufnfv  5946  f1eqcocnv  5994  nfriotad  6055  riotaprop  6071  oprabid  6110  elrnmpt2  6198  ov6g  6223  ovelrn  6234  caovmo  6295  offn  6326  caofinvl  6342  fr3nr  6386  onprc  6391  ordeleqon  6395  onint0  6402  0elsuc  6441  onuninsuci  6446  orduninsuc  6449  ordzsl  6451  onzsl  6452  tfinds  6465  limomss  6476  limom  6486  peano5  6494  xpexr  6513  eqop2  6612  1stconst  6656  2ndconst  6657  funsssuppss  6710  dftpos3  6758  dftpos4  6759  oawordeulem  6985  omwordi  7002  nnmwordi  7066  riiner  7165  ecopover  7196  map0g  7244  mapsn  7246  elixpsn  7294  en0  7364  en1  7368  fiprc  7383  sbthlem2  7414  sbthlem4  7416  sbthlem5  7417  nneneq  7486  sdom1  7504  fineqvlem  7519  nfielex  7533  findcard  7543  findcard2  7544  elfiun  7672  marypha1lem  7675  oicl  7735  oif  7736  oion  7742  hartogslem1  7748  hartogs  7750  wemapso2  7760  card2on  7761  0wdom  7777  brwdom2  7780  sucprcregOLD  7807  inf3lem6  7831  noinfepOLD  7858  cantnflem3  7891  cantnflem4  7892  cantnflem3OLD  7913  cantnflem4OLD  7914  wemapwe  7920  wemapweOLD  7921  cnfcom  7925  cnfcomOLD  7933  tctr  7952  r1tr  7975  r1rankidb  8003  r1pw  8044  scottex  8084  scott0  8085  bnd2  8092  tskwe  8112  oncard  8122  cardlim  8134  harsdom  8157  en2eleq  8167  dfac8alem  8191  cardaleph  8251  iunfictbso  8276  infmap2  8379  ackbij1lem18  8398  cff  8409  cfsuc  8418  cff1  8419  cflim2  8424  cfss  8426  sdom2en01  8463  infpssrlem4  8467  fin23lem7  8477  fin23lem11  8478  isfin2-2  8480  fin23lem26  8486  fin23lem19  8497  fin23lem17  8499  isf34lem2  8534  isf34lem4  8538  fin1a2lem6  8566  fin1a2lem10  8570  fin1a2lem12  8572  itunifn  8578  hsmexlem1  8587  axcc2lem  8597  dcomex  8608  axdc3lem4  8614  ondomon  8719  konigthlem  8724  pwcfsdom  8739  cfpwsdom  8740  axpowndlem3  8756  axpowndlem3OLD  8757  canth4  8806  canthnumlem  8807  canthwelem  8809  canthwe  8810  canthp1lem2  8812  pwfseqlem4  8821  pwfseqlem5  8822  gchaleph  8830  gch2  8834  winainflem  8852  0tsk  8914  rankcf  8936  tskcard  8940  gruina  8977  grutsk  8981  tskmid  8999  indpi  9068  nqereu  9090  mulcanenq  9121  recmulnq  9125  archnq  9141  ltsopr  9193  1ne0sr  9255  0idsr  9256  00sr  9258  leid  9462  lelttric  9473  divcan3  10010  lemul1a  10175  nn1suc  10335  nn0n0n1ge2b  10636  nn0ind-raph  10734  elnn1uz2  10923  indstr2  10925  uzsupss  10939  rpnnen1lem4  10974  rpnnen1lem5  10975  xrnemnf  11091  xrnepnf  11092  mnfltxr  11099  nn0pnfge0  11104  xrlttri  11108  xrlttr  11109  xrleid  11119  qbtwnxr  11162  xmullem2  11220  xlemul1a  11243  xrub  11266  ixxun  11308  fztpval  11510  fseq1p1m1  11526  elfznelfzob  11623  ltweuz  11776  fzfi  11786  ser0f  11851  0exp  11891  faclbnd4lem1  12061  bcn1  12081  hashnemnf  12107  hashv01gt1  12108  hashle00  12150  hashgt12el2  12166  hash2prd  12173  hashmap  12189  hashpw  12190  hashf1  12202  fz1isolem  12206  0wrd0  12245  ccatvalfn  12272  swrdlen  12311  swrdvalfn  12324  swrdspsleq  12334  cats1un  12362  wrdind  12363  wrd2ind  12364  swrdccatin1  12366  repswsymballbi  12410  cshw1  12448  sqr0lem  12722  sqrsq  12751  mptfzshft  13237  fsumrev  13238  egt2lt3  13480  0dvds  13545  bitsp1o  13621  gcddvds  13691  bezout  13718  1nprm  13760  prmind2  13766  rpdvds  13802  pcpre1  13901  vdwapf  14025  vdwapid1  14028  ram0  14075  ramz  14078  cshws0  14120  prmlem0  14125  strle1  14261  restsspw  14362  prdsdsfn  14395  imasdsfn  14444  imasaddfnlem  14458  imasvscafn  14467  xpscfv  14492  xpsfrnel  14493  isacs1i  14587  cidfn  14609  comffn  14636  isoval  14695  sscres  14728  cofucl  14790  idffth  14835  ressffth  14840  catcoppccl  14968  1stfcl  14999  2ndfcl  15000  prfcl  15005  evlfcl  15024  curf1cl  15030  curfcl  15034  hofcl  15061  yonedainv  15083  pospo  15135  lubfun  15142  glbfun  15155  joindmss  15169  meetdmss  15183  ipopos  15322  acsficl2d  15338  dirref  15397  mgmidcl  15428  mgmlrid  15429  cntzssv  15837  symggrp  15896  symgid  15897  idresperm  15905  pmtrfmvdn0  15959  symggen  15967  psgnunilem1  15990  psgnprfval  16016  slwpgp  16103  frgpmhm  16253  frgpuptinv  16259  frgpup3lem  16265  gsumcom2  16457  abv0  16896  rrgsupp  17342  psrvscafval  17441  psrridm  17456  psrridmOLD  17457  ltbwe  17534  psrbag0  17556  psrbagsn  17557  subrgascl  17560  zrhrhm  17923  psgnodpmr  18000  frlmphl  18186  ellspd  18210  ellspdOLD  18211  mattpostpos  18318  mavmul0  18343  mavmul0g  18344  mdet0f1o  18384  m2detleiblem5  18411  m2detleiblem6  18412  m2detleiblem3  18415  m2detleiblem4  18416  maducoeval2  18426  baspartn  18539  eltg3  18547  fctop  18588  cctop  18590  discld  18673  mretopd  18676  neipeltop  18713  neitr  18764  restcls  18765  ordtbaslem  18772  ordtuni  18774  idcn  18841  cnrmi  18944  cmpsublem  18982  cmpsub  18983  tgcmp  18984  uncmp  18986  hauscmplem  18989  cmpfi  18991  bwth  18993  bwthOLD  18994  1stcrestlem  19036  disllycmp  19082  dis1stc  19083  kgeni  19090  1stckgenlem  19106  kqffn  19278  snfil  19417  filcon  19436  cfinfil  19446  ufileu  19472  filufint  19473  fixufil  19475  cfinufil  19481  ufilen  19483  fin1aufil  19485  fmf  19498  rnelfm  19506  flimclslem  19537  hauspwpwf1  19540  supnfcls  19573  flimfnfcls  19581  fclscmp  19583  alexsubALTlem2  19600  alexsubALTlem3  19601  alexsubALT  19603  ptcmplem1  19604  cnextrel  19615  tsmsfbas  19678  ustref  19773  trust  19784  restutop  19792  isusp  19816  xmet0  19897  imasdsf1olem  19928  blfvalps  19938  blfps  19961  blf  19962  restmetu  20142  dscmet  20145  isngp2  20169  nm0  20198  nrginvrcn  20252  nmoix  20288  qdensere  20329  iccconn  20387  iccpnfcnv  20496  xrhmeo  20498  lebnumlem3  20515  cmetss  20805  bcthlem5  20819  rrxmfval  20885  minveclem3b  20895  cniccbdd  20925  ovolicc2lem4  20983  iunmbl  21014  ioorinv  21036  ioorcl  21037  i1f1lem  21147  limcvallem  21326  ellimc2  21332  limccnp  21346  limccnp2  21347  limcco  21348  perfdvf  21358  recnprss  21359  fncpn  21387  dvcmulf  21399  c1lip1  21449  lhop2  21467  q1pcl  21607  r1pdeglt  21610  ply1remlem  21614  plyssc  21648  ulm0  21836  cxpeq0  22103  cxplea  22121  asinlem  22243  isppw2  22433  muval2  22452  dchrfi  22574  dchrpt  22586  bposlem6  22608  lgsdir2lem2  22643  lgsqr  22665  2sqlem7  22689  2sqlem11  22694  chtppilim  22704  tgldimor  22935  tglnfn  22961  tglnunirn  22962  mircinv  23049  xmstrkgc  23100  axcgrtr  23129  axsegconlem9  23139  axlowdimlem5  23160  axlowdimlem17  23172  axlowdim1  23173  uhgra0  23211  uhgra0v  23212  umgra0  23227  usgra0  23257  usgra0v  23258  usgraedg4  23273  usgra1v  23276  nb3graprlem1  23327  cusgra1v  23337  cusgraexilem2  23343  uvtx01vtx  23368  wlkntrl  23429  0spth  23438  1pthonlem1  23456  2pthlem1  23462  3v3e3cycl1  23498  constr3trllem1  23504  constr3pthlem3  23511  4cycl4v4e  23520  4cycl4dv  23521  0conngra  23528  ex-opab  23607  grpoinvf  23695  ismgm  23775  rngomndo  23876  nvmid  24013  nmlnoubi  24164  hiidrcl  24465  hsn0elch  24619  shjshseli  24864  cmbr4i  24972  dfiop2  25125  kbpj  25328  nmopun  25386  adjeq0  25463  kbass2  25489  pjssdif1i  25547  pjinvari  25563  pjcmul2i  25574  pj3i  25580  stge1i  25610  stle0i  25611  sumdmdlem2  25791  dmdbr6ati  25795  dmdbr7ati  25796  rabsnel  25855  disjdifprg  25887  ofoprabco  25950  fpwrelmapffslem  26000  xrlelttric  26013  iundisj2cnt  26051  nn0min  26058  xrge0tsmsbi  26222  pstmxmet  26293  xrge0iifcnv  26332  xrge0iif1  26337  qqhre  26415  esumcl  26455  esumpr2  26486  esumpinfval  26491  esumpcvgval  26496  ofcfn  26511  pwsiga  26542  prsiga  26543  sigainb  26548  measiuns  26600  relfae  26632  sitgf  26702  eulerpartgbij  26724  sgnmulsgn  26901  sgnmulsgp  26902  plymulx  26918  signswch  26931  signslema  26932  signstlen  26937  subfacp1lem5  27041  erdszelem8  27055  kur14lem1  27063  indispcon  27092  cvmsss2  27132  relexpsucr  27301  prodf1f  27376  fprodshft  27456  fprodrev  27457  dfpo2  27534  dfon2lem7  27571  wfrlem4  27696  wfrlem14  27706  frrlem6  27746  nosgnn0i  27769  nobndlem2  27803  nobndlem4  27805  nobndlem5  27806  nobndlem6  27807  brbigcup  27898  elsingles  27918  fnimage  27929  funpartlem  27942  dfrdg4  27950  imagesset  27953  altopthsn  27961  elaltxp  27975  ellines  28152  linethru  28153  rankeq1o  28178  elhf2  28182  hfninf  28193  limsucncmpi  28261  volsupnfl  28407  cnambfre  28411  dvasin  28451  dvacos  28452  nn0prpwlem  28488  fneref  28527  refref  28528  neibastop2lem  28552  sdclem2  28609  sstotbnd2  28644  ssbnd  28658  grpokerinj  28721  isdrngo1  28733  ac6s6  28955  prtlem12  28983  elrfirn  29002  ismrcd1  29005  istopclsd  29007  rabren3dioph  29125  jm2.17b  29275  jm2.22  29315  jm2.23  29316  ttac  29356  pw2f1ocnv  29357  dnnumch1  29368  hbtlem5  29455  mncn0  29467  aaitgo  29490  rngunsnply  29501  ssrecnpr  29565  seff  29566  sblpnf  29567  dvconstbi  29579  ipo0  29676  ifr0  29677  addrfn  29699  subrfn  29700  mulvfn  29701  refsum2cnlem1  29730  stoweidlem26  29792  stoweidlem50  29816  stoweidlem57  29823  2ffzoeq  30185  hash2prv  30197  wrdlen1  30221  wlkcomp  30257  wwlkn0s  30310  clwlkcomp  30397  frgra0v  30556  frgra1v  30561  1vwmgra  30566  vdgfrgragt2  30591  frgrancvvdeqlem3  30596  frgrawopreg1  30614  frgrawopreg2  30615  2spot0  30628  fsuppmapnn0fiubex  30769  m1detdiag  30865  zlmodzxzldeplem4  30976  bnj145OLD  31647  bnj216  31652  bnj151  31799  bnj517  31807  bnj970  31869  bnj1014  31882  bnj1145  31913  bnj1498  31981  bj-dedthm  32024  bj-speiv  32122  bj-exlimmpbir  32314  bj-snglex  32366  bj-inftyexpidisj  32433  riotasv2d  32501  lkrscss  32636  islshpkrN  32658  isline  33276  ispointN  33279  0psubN  33286  linepsubN  33289  atpsubN  33290  cdlemk36  34450  diafn  34572  dibfna  34692  dibvalrel  34701  dicvalrelN  34723  diclspsn  34732  dihvalrel  34817  dih1  34824  lclkrlem1  35044  lclkr  35071  mapd1o  35186  mapdin  35200  hdmapfnN  35370  hgmapfnN  35429
  Copyright terms: Public domain W3C validator