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  955  spei  1996  nfald2  2057  nfabd2  2624  dedhb  3253  sbceqal  3367  ssdifeq0  3893  r19.2zb  3902  dedth  3975  pwidg  4007  elpr2  4030  snidg  4037  exsnrex  4049  ifpr  4059  rabrsn  4082  prid1g  4118  pwpw0  4160  sssn  4170  preqr1  4186  pwsnALT  4226  unimax  4267  intmin3  4297  syl6eqbr  4471  intabs  4595  pwnss  4599  0inp0  4606  copsexg  4719  copsexgOLD  4720  euotd  4735  elopab  4742  epelg  4779  ord0eln0  4919  sucidg  4943  nsuceq0  4945  onun2i  4980  elvvuni  5047  posn  5055  frsn  5057  eqrelriv  5083  relopabi  5115  opabid2  5119  ididg  5143  iss  5308  funopg  5607  fn0  5687  f00  5754  f0bi  5755  f1o00  5835  fo00  5836  brprcneu  5846  dffn5  5900  fsn  6051  fnsnb  6072  fconstfvOLD  6116  eufnfv  6128  f1eqcocnv  6186  nfriotad  6247  riotaprop  6263  oprabid  6305  elrnmpt2  6397  ov6g  6422  ovelrn  6433  caovmo  6494  offn  6533  caofinvl  6549  fr3nr  6597  onprc  6602  ordeleqon  6606  onint0  6613  0elsuc  6652  onuninsuci  6657  orduninsuc  6660  ordzsl  6662  onzsl  6663  tfinds  6676  limomss  6687  limom  6697  peano5  6705  xpexr  6722  eqop2  6823  1stconst  6870  2ndconst  6871  funsssuppss  6925  dftpos3  6972  dftpos4  6973  oawordeulem  7202  omwordi  7219  nnmwordi  7283  riiner  7383  ecopover  7414  map0g  7457  mapsn  7459  elixpsn  7507  en0  7577  en1  7581  fiprc  7596  sbthlem2  7627  sbthlem4  7629  sbthlem5  7630  nneneq  7699  sdom1  7718  fineqvlem  7733  nfielex  7747  findcard  7758  findcard2  7759  elfiun  7889  marypha1lem  7892  oicl  7954  oif  7955  oion  7961  hartogslem1  7967  hartogs  7969  wemapso2  7979  card2on  7980  0wdom  7996  brwdom2  7999  sucprcregOLD  8026  inf3lem6  8050  noinfepOLD  8077  cantnflem3  8110  cantnflem4  8111  cantnflem3OLD  8132  cantnflem4OLD  8133  wemapwe  8139  wemapweOLD  8140  cnfcom  8144  cnfcomOLD  8152  tctr  8171  r1tr  8194  r1rankidb  8222  r1pw  8263  scottex  8303  scott0  8304  bnd2  8311  tskwe  8331  oncard  8341  cardlim  8353  harsdom  8376  en2eleq  8386  dfac8alem  8410  cardaleph  8470  iunfictbso  8495  infmap2  8598  ackbij1lem18  8617  cff  8628  cfsuc  8637  cff1  8638  cflim2  8643  cfss  8645  sdom2en01  8682  infpssrlem4  8686  fin23lem7  8696  fin23lem11  8697  isfin2-2  8699  fin23lem26  8705  fin23lem19  8716  fin23lem17  8718  isf34lem2  8753  isf34lem4  8757  fin1a2lem6  8785  fin1a2lem10  8789  fin1a2lem12  8791  itunifn  8797  hsmexlem1  8806  axcc2lem  8816  dcomex  8827  axdc3lem4  8833  ondomon  8938  konigthlem  8943  pwcfsdom  8958  cfpwsdom  8959  axpowndlem3  8975  axpowndlem3OLD  8976  canth4  9025  canthnumlem  9026  canthwelem  9028  canthwe  9029  canthp1lem2  9031  pwfseqlem4  9040  pwfseqlem5  9041  gchaleph  9049  gch2  9053  winainflem  9071  0tsk  9133  rankcf  9155  tskcard  9159  gruina  9196  grutsk  9200  tskmid  9218  indpi  9285  nqereu  9307  mulcanenq  9338  recmulnq  9342  archnq  9358  ltsopr  9410  1ne0sr  9473  0idsr  9474  00sr  9476  leid  9680  lelttric  9691  divcan3  10234  lemul1a  10399  nn1suc  10560  nn0n0n1ge2b  10863  nn0lt10b  10928  nn0ind-raph  10966  elnn1uz2  11164  indstr2  11166  uzsupss  11180  rpnnen1lem4  11217  rpnnen1lem5  11218  xrnemnf  11334  xrnepnf  11335  mnfltxr  11342  nn0pnfge0  11347  xrlttri  11351  xrlttr  11352  xrleid  11362  qbtwnxr  11405  xmullem2  11463  xlemul1a  11486  xrub  11509  ixxun  11551  fztpval  11747  fseq1p1m1  11758  elfznelfzob  11892  ltweuz  12048  fzfi  12058  fsuppmapnn0fiubex  12074  ser0f  12136  0exp  12177  faclbnd4lem1  12347  bcn1  12367  hashnemnf  12393  hashv01gt1  12394  hashle00  12441  hashgt12el2  12458  hashmap  12469  hashpw  12470  hashf1  12482  fz1isolem  12486  hash2prd  12494  hash2prv  12501  0wrd0  12542  wrdlen1  12555  ccatvalfn  12575  swrdlen  12626  swrdvalfn  12639  swrdspsleq  12649  cats1un  12677  wrdind  12678  wrd2ind  12679  swrdccatin1  12684  repswsymballbi  12728  cshw1  12766  scshwfzeqfzo  12770  sqr0lem  13050  sqrtsq  13079  mptfzshft  13569  fsumrev  13570  egt2lt3  13813  0dvds  13878  bitsp1o  13957  gcddvds  14027  bezout  14054  1nprm  14096  prmind2  14102  rpdvds  14139  pcpre1  14240  vdwapf  14364  vdwapid1  14367  ram0  14414  ramz  14417  cshws0  14460  prmlem0  14465  strle1  14602  restsspw  14703  prdsdsfn  14736  imasdsfn  14785  imasaddfnlem  14799  imasvscafn  14808  xpscfv  14833  xpsfrnel  14834  isacs1i  14928  cidfn  14950  comffn  14974  isoval  15033  sscres  15066  cofucl  15128  idffth  15173  ressffth  15178  catcoppccl  15306  1stfcl  15337  2ndfcl  15338  prfcl  15343  evlfcl  15362  curf1cl  15368  curfcl  15372  hofcl  15399  yonedainv  15421  pospo  15474  lubfun  15481  glbfun  15494  joindmss  15508  meetdmss  15522  ipopos  15661  acsficl2d  15677  dirref  15736  mgmidcl  15763  mgmlrid  15764  cntzssv  16237  symggrp  16296  symgid  16297  idresperm  16305  pmtrfmvdn0  16358  symggen  16366  psgnunilem1  16389  psgnprfval  16417  slwpgp  16504  frgpmhm  16654  frgpuptinv  16660  frgpup3lem  16666  gsumzoppg  16838  gsumcom2  16874  abv0  17351  rrgsupp  17810  psrvscafval  17914  psrridm  17929  psrridmOLD  17930  ltbwe  18008  psrbag0  18030  psrbagsn  18031  subrgascl  18034  zrhrhm  18419  psgnodpmr  18496  frlmphl  18682  ellspd  18706  ellspdOLD  18707  mattpostpos  18826  mavmul0  18924  mavmul0g  18925  mdet0f1o  18965  m1detdiag  18969  m2detleiblem5  18997  m2detleiblem6  18998  m2detleiblem3  19001  m2detleiblem4  19002  maducoeval2  19012  d1mat2pmat  19110  chpmat1dlem  19206  chpmat1d  19207  baspartn  19325  eltg3  19333  fctop  19375  cctop  19377  discld  19460  mretopd  19463  neipeltop  19500  neitr  19551  restcls  19552  ordtbaslem  19559  ordtuni  19561  idcn  19628  cnrmi  19731  cmpsublem  19769  cmpsub  19770  tgcmp  19771  uncmp  19773  hauscmplem  19776  cmpfi  19778  bwth  19780  bwthOLD  19781  1stcrestlem  19823  disllycmp  19869  dis1stc  19870  refref  19884  kgeni  19908  1stckgenlem  19924  kqffn  20096  snfil  20235  filcon  20254  cfinfil  20264  ufileu  20290  filufint  20291  fixufil  20293  cfinufil  20299  ufilen  20301  fin1aufil  20303  fmf  20316  rnelfm  20324  flimclslem  20355  hauspwpwf1  20358  supnfcls  20391  flimfnfcls  20399  fclscmp  20401  alexsubALTlem2  20418  alexsubALTlem3  20419  alexsubALT  20421  ptcmplem1  20422  cnextrel  20433  tsmsfbas  20496  ustref  20591  trust  20602  restutop  20610  isusp  20634  xmet0  20715  imasdsf1olem  20746  blfvalps  20756  blfps  20779  blf  20780  restmetu  20960  dscmet  20963  isngp2  20987  nm0  21016  nrginvrcn  21070  nmoix  21106  qdensere  21147  iccconn  21205  iccpnfcnv  21314  xrhmeo  21316  lebnumlem3  21333  cmetss  21623  bcthlem5  21637  rrxmfval  21703  minveclem3b  21713  cniccbdd  21743  ovolicc2lem4  21801  iunmbl  21833  ioorinv  21855  ioorcl  21856  i1f1lem  21966  limcvallem  22145  ellimc2  22151  limccnp  22165  limccnp2  22166  limcco  22167  perfdvf  22177  recnprss  22178  fncpn  22206  dvcmulf  22218  c1lip1  22268  lhop2  22286  q1pcl  22426  r1pdeglt  22429  ply1remlem  22433  plyssc  22467  ulm0  22655  cxpeq0  22928  cxplea  22946  asinlem  23068  isppw2  23258  muval2  23277  dchrfi  23399  dchrpt  23411  bposlem6  23433  lgsdir2lem2  23468  lgsqr  23490  2sqlem7  23514  2sqlem11  23519  chtppilim  23529  tgldimor  23762  tglnfn  23803  tglnunirn  23804  mircinv  23917  perpln1  23956  perpln2  23957  lmiisolem  24030  xmstrkgc  24058  axcgrtr  24087  axsegconlem9  24097  axlowdimlem5  24118  axlowdimlem17  24130  axlowdim1  24131  uhgra0  24178  uhgra0v  24179  umgra0  24194  usgra0  24239  usgra0v  24240  usgraedg4  24256  usgra1v  24259  nb3graprlem1  24320  cusgra1v  24330  cusgraexilem2  24336  uvtx01vtx  24361  wlkcomp  24394  wlkntrl  24433  0spth  24442  1pthonlem1  24460  2pthlem1  24466  usgra2wlkspthlem1  24488  3v3e3cycl1  24513  constr3trllem1  24519  constr3pthlem3  24526  4cycl4v4e  24535  4cycl4dv  24536  0conngra  24543  wwlkn0s  24574  clwlkcomp  24632  frgra0v  24862  frgra1v  24867  1vwmgra  24872  vdgfrgragt2  24896  frgrancvvdeqlem3  24901  frgrawopreg1  24919  frgrawopreg2  24920  2spot0  24933  ex-opab  25022  grpoinvf  25111  ismgmOLD  25191  rngomndo  25292  nvmid  25429  nmlnoubi  25580  hiidrcl  25881  hsn0elch  26035  shjshseli  26280  cmbr4i  26388  dfiop2  26541  kbpj  26744  nmopun  26802  adjeq0  26879  kbass2  26905  pjssdif1i  26963  pjinvari  26979  pjcmul2i  26990  pj3i  26996  stge1i  27026  stle0i  27027  sumdmdlem2  27207  dmdbr6ati  27211  dmdbr7ati  27212  rabsnel  27271  disjdifprg  27305  ofoprabco  27374  fpwrelmapffslem  27424  xrlelttric  27441  iundisj2cnt  27473  nn0min  27481  xrge0tsmsbi  27646  locfinref  27714  dispcmp  27732  pstmxmet  27746  xrge0iifcnv  27785  xrge0iif1  27790  qqhre  27868  esumcl  27913  esumpr2  27944  esumpinfval  27949  esumpcvgval  27954  ofcfn  27969  pwsiga  28000  prsiga  28001  sigainb  28006  measiuns  28058  relfae  28089  sitgf  28159  eulerpartgbij  28181  sgnmulsgn  28358  sgnmulsgp  28359  signswch  28388  signslema  28389  signstlen  28394  subfacp1lem5  28498  erdszelem8  28512  kur14lem1  28520  indispcon  28549  cvmsss2  28589  msubrn  28759  relexpsucr  28923  prodf1f  28998  fprodrev  29079  dfpo2  29156  dfon2lem7  29193  wfrlem4  29318  wfrlem14  29328  frrlem6  29368  nosgnn0i  29391  nobndlem2  29425  nobndlem4  29427  nobndlem5  29428  nobndlem6  29429  brbigcup  29520  elsingles  29540  fnimage  29551  funpartlem  29564  dfrdg4  29572  imagesset  29575  altopthsn  29583  elaltxp  29597  ellines  29774  linethru  29775  rankeq1o  29800  elhf2  29804  hfninf  29815  limsucncmpi  29882  volsupnfl  30031  cnambfre  30035  dvasin  30075  dvacos  30076  nn0prpwlem  30112  fneref  30140  neibastop2lem  30150  sdclem2  30207  sstotbnd2  30242  ssbnd  30256  grpokerinj  30319  isdrngo1  30331  ac6s6  30552  prtlem12  30580  elrfirn  30599  ismrcd1  30602  istopclsd  30604  rabren3dioph  30721  jm2.17b  30871  jm2.22  30909  jm2.23  30910  ttac  30950  pw2f1ocnv  30951  dnnumch1  30962  hbtlem5  31049  mncn0  31061  aaitgo  31084  rngunsnply  31095  ssrecnpr  31161  seff  31162  sblpnf  31163  lcmdvds  31187  nzss  31195  dvconstbi  31212  ipo0  31309  ifr0  31310  addrfn  31332  subrfn  31333  mulvfn  31334  refsum2cnlem1  31363  ellimciota  31528  dvmptconst  31614  dvmptidg  31616  dvmulcncf  31626  dvdivcncf  31628  stoweidlem26  31697  stoweidlem50  31721  stoweidlem57  31728  2ffzoeq  32179  uhguhgra  32210  uhg0e  32214  uhgres  32217  fusgraimpcl  32265  fusgraimpclALT  32267  0mgm  32300  nnsgrpmgm  32341  fnhomeqhomf  32430  estrchomfn  32487  funcestrcsetclem4  32495  funcestrcsetclem7  32498  rngchomffvalOLD  32540  funcringcsetcOLD2lem4  32579  funcringcsetclem4OLD  32602  srhmsubc  32612  rhmsubclem1  32622  srhmsubcOLD  32631  rhmsubcOLDlem1  32641  mapsnop  32662  zlmodzxzldeplem4  32834  bnj145OLD  33510  bnj216  33515  bnj151  33663  bnj517  33671  bnj970  33733  bnj1145  33777  bnj1498  33845  bj-dedthm  33895  bj-speiv  34020  bj-exlimmpbir  34212  bj-snglex  34264  bj-inftyexpidisj  34336  riotasv2d  34411  lkrscss  34546  islshpkrN  34568  isline  35186  ispointN  35189  0psubN  35196  linepsubN  35199  atpsubN  35200  cdlemk36  36362  diafn  36484  dibfna  36604  dibvalrel  36613  dicvalrelN  36635  diclspsn  36644  dihvalrel  36729  dih1  36736  lclkrlem1  36956  lclkr  36983  mapd1o  37098  mapdin  37112  hdmapfnN  37282  hgmapfnN  37341
  Copyright terms: Public domain W3C validator