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, 5-Aug-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  941  spei  1955  nfald2  2022  nfabd2  2587  dedhb  3118  sbceqal  3230  sbcel12  3663  ssdifeq0  3749  r19.2zb  3758  dedth  3829  pwidg  3861  elpr2  3884  snidg  3891  exsnrex  3902  ifpr  3912  rabrsn  3933  prid1g  3969  pwpw0  4009  sssn  4019  preqr1  4034  pwsnALT  4074  unimax  4115  intmin3  4144  syl6eqbr  4317  intabs  4441  pwnss  4445  0inp0  4452  copsexg  4564  copsexgOLD  4565  euotd  4580  elopab  4585  epelg  4620  ord0eln0  4760  sucidg  4784  nsuceq0  4786  onun2i  4821  elvvuni  4886  posn  4894  frsn  4896  eqrelriv  4920  relopabi  4952  opabid2  4956  ididg  4980  iss  5142  funopg  5438  fn0  5518  f00  5581  f0bi  5582  f1o00  5661  fo00  5662  brprcneu  5672  dffn5  5725  fsn  5868  fnsnb  5885  fconstfv  5927  eufnfv  5938  f1eqcocnv  5986  nfriotad  6048  riotaprop  6064  oprabid  6104  elrnmpt2  6192  ov6g  6217  ovelrn  6228  caovmo  6289  offn  6320  caofinvl  6336  fr3nr  6380  onprc  6385  ordeleqon  6389  onint0  6396  0elsuc  6435  onuninsuci  6440  orduninsuc  6443  ordzsl  6445  onzsl  6446  tfinds  6459  limomss  6470  limom  6480  peano5  6488  xpexr  6507  eqop2  6606  1stconst  6650  2ndconst  6651  funsssuppss  6704  dftpos3  6752  dftpos4  6753  oawordeulem  6981  omwordi  6998  nnmwordi  7062  riiner  7161  ecopover  7192  map0g  7240  mapsn  7242  elixpsn  7290  en0  7360  en1  7364  fiprc  7379  sbthlem2  7410  sbthlem4  7412  sbthlem5  7413  nneneq  7482  sdom1  7500  fineqvlem  7515  nfielex  7529  findcard  7539  findcard2  7540  elfiun  7668  marypha1lem  7671  oicl  7731  oif  7732  oion  7738  hartogslem1  7744  hartogs  7746  wemapso2  7756  card2on  7757  0wdom  7773  brwdom2  7776  sucprcregOLD  7803  inf3lem6  7827  noinfepOLD  7854  cantnflem3  7887  cantnflem4  7888  cantnflem3OLD  7909  cantnflem4OLD  7910  wemapwe  7916  wemapweOLD  7917  cnfcom  7921  cnfcomOLD  7929  tctr  7948  r1tr  7971  r1rankidb  7999  r1pw  8040  scottex  8080  scott0  8081  bnd2  8088  tskwe  8108  oncard  8118  cardlim  8130  harsdom  8153  en2eleq  8163  dfac8alem  8187  cardaleph  8247  iunfictbso  8272  infmap2  8375  ackbij1lem18  8394  cff  8405  cfsuc  8414  cff1  8415  cflim2  8420  cfss  8422  sdom2en01  8459  infpssrlem4  8463  fin23lem7  8473  fin23lem11  8474  isfin2-2  8476  fin23lem26  8482  fin23lem19  8493  fin23lem17  8495  isf34lem2  8530  isf34lem4  8534  fin1a2lem6  8562  fin1a2lem10  8566  fin1a2lem12  8568  itunifn  8574  hsmexlem1  8583  axcc2lem  8593  dcomex  8604  axdc3lem4  8610  ondomon  8715  konigthlem  8720  pwcfsdom  8735  cfpwsdom  8736  axpowndlem3  8752  axpowndlem3OLD  8753  canth4  8801  canthnumlem  8802  canthwelem  8804  canthwe  8805  canthp1lem2  8807  pwfseqlem4  8816  pwfseqlem5  8817  gchaleph  8825  gch2  8829  winainflem  8847  0tsk  8909  rankcf  8931  tskcard  8935  gruina  8972  grutsk  8976  tskmid  8994  indpi  9063  nqereu  9085  mulcanenq  9116  recmulnq  9120  archnq  9136  ltsopr  9188  1ne0sr  9250  0idsr  9251  00sr  9253  leid  9457  lelttric  9468  divcan3  10005  lemul1a  10170  nn1suc  10330  nn0n0n1ge2b  10631  nn0ind-raph  10729  elnn1uz2  10918  indstr2  10920  uzsupss  10934  rpnnen1lem4  10969  rpnnen1lem5  10970  xrnemnf  11086  xrnepnf  11087  mnfltxr  11094  nn0pnfge0  11099  xrlttri  11103  xrlttr  11104  xrleid  11114  qbtwnxr  11157  xmullem2  11215  xlemul1a  11238  xrub  11261  ixxun  11303  fztpval  11501  fseq1p1m1  11517  elfznelfzob  11614  ltweuz  11767  fzfi  11777  ser0f  11842  0exp  11882  faclbnd4lem1  12052  bcn1  12072  hashnemnf  12098  hashv01gt1  12099  hashle00  12141  hashgt12el2  12157  hash2prd  12164  hashmap  12180  hashpw  12181  hashf1  12193  fz1isolem  12197  0wrd0  12236  ccatvalfn  12263  swrdlen  12302  swrdvalfn  12315  swrdspsleq  12325  cats1un  12353  wrdind  12354  wrd2ind  12355  swrdccatin1  12357  repswsymballbi  12401  cshw1  12439  sqr0lem  12713  sqrsq  12742  fsumrev  13228  fsumshft  13229  egt2lt3  13470  0dvds  13535  bitsp1o  13611  gcddvds  13681  bezout  13708  1nprm  13750  prmind2  13756  rpdvds  13792  pcpre1  13891  vdwapf  14015  vdwapid1  14018  ram0  14065  ramz  14068  cshws0  14110  prmlem0  14115  strle1  14251  restsspw  14352  prdsdsfn  14385  imasdsfn  14434  imasaddfnlem  14448  imasvscafn  14457  xpscfv  14482  xpsfrnel  14483  isacs1i  14577  cidfn  14599  comffn  14626  isoval  14685  sscres  14718  cofucl  14780  idffth  14825  ressffth  14830  catcoppccl  14958  1stfcl  14989  2ndfcl  14990  prfcl  14995  evlfcl  15014  curf1cl  15020  curfcl  15024  hofcl  15051  yonedainv  15073  pospo  15125  lubfun  15132  glbfun  15145  joindmss  15159  meetdmss  15173  ipopos  15312  acsficl2d  15328  dirref  15387  mgmidcl  15418  mgmlrid  15419  cntzssv  15825  symggrp  15884  symgid  15885  idresperm  15893  pmtrfmvdn0  15947  symggen  15955  psgnunilem1  15978  psgnprfval  16004  slwpgp  16091  frgpmhm  16241  frgpuptinv  16247  frgpup3lem  16253  gsumcom2  16440  abv0  16839  rrgsupp  17283  psrvscafval  17394  psrridm  17409  psrridmOLD  17410  ltbwe  17485  psrbag0  17507  psrbagsn  17508  subrgascl  17511  zrhrhm  17784  psgnodpmr  17861  frlmphl  18047  ellspd  18071  ellspdOLD  18072  mattpostpos  18179  mavmul0  18204  mavmul0g  18205  mdet0f1o  18245  m2detleiblem5  18272  m2detleiblem6  18273  m2detleiblem3  18276  m2detleiblem4  18277  maducoeval2  18287  baspartn  18400  eltg3  18408  fctop  18449  cctop  18451  discld  18534  mretopd  18537  neipeltop  18574  neitr  18625  restcls  18626  ordtbaslem  18633  ordtuni  18635  idcn  18702  cnrmi  18805  cmpsublem  18843  cmpsub  18844  tgcmp  18845  uncmp  18847  hauscmplem  18850  cmpfi  18852  bwth  18854  bwthOLD  18855  1stcrestlem  18897  disllycmp  18943  dis1stc  18944  kgeni  18951  1stckgenlem  18967  kqffn  19139  snfil  19278  filcon  19297  cfinfil  19307  ufileu  19333  filufint  19334  fixufil  19336  cfinufil  19342  ufilen  19344  fin1aufil  19346  fmf  19359  rnelfm  19367  flimclslem  19398  hauspwpwf1  19401  supnfcls  19434  flimfnfcls  19442  fclscmp  19444  alexsubALTlem2  19461  alexsubALTlem3  19462  alexsubALT  19464  ptcmplem1  19465  cnextrel  19476  tsmsfbas  19539  ustref  19634  trust  19645  restutop  19653  isusp  19677  xmet0  19758  imasdsf1olem  19789  blfvalps  19799  blfps  19822  blf  19823  restmetu  20003  dscmet  20006  isngp2  20030  nm0  20059  nrginvrcn  20113  nmoix  20149  qdensere  20190  iccconn  20248  iccpnfcnv  20357  xrhmeo  20359  lebnumlem3  20376  cmetss  20666  bcthlem5  20680  rrxmfval  20746  minveclem3b  20756  cniccbdd  20786  ovolicc2lem4  20844  iunmbl  20875  ioorinv  20897  ioorcl  20898  i1f1lem  21008  limcvallem  21187  ellimc2  21193  limccnp  21207  limccnp2  21208  limcco  21209  perfdvf  21219  recnprss  21220  fncpn  21248  dvcmulf  21260  c1lip1  21310  lhop2  21328  q1pcl  21511  r1pdeglt  21514  ply1remlem  21518  plyssc  21552  ulm0  21740  cxpeq0  22007  cxplea  22025  asinlem  22147  isppw2  22337  muval2  22356  dchrfi  22478  dchrpt  22490  bposlem6  22512  lgsdir2lem2  22547  lgsqr  22569  2sqlem7  22593  2sqlem11  22598  chtppilim  22608  tgldimor  22836  tglnfn  22861  tglnunirn  22862  xmstrkgc  22954  axcgrtr  22983  axsegconlem9  22993  axlowdimlem5  23014  axlowdimlem17  23026  axlowdim1  23027  uhgra0  23065  uhgra0v  23066  umgra0  23081  usgra0  23111  usgra0v  23112  usgraedg4  23127  usgra1v  23130  nb3graprlem1  23181  cusgra1v  23191  cusgraexilem2  23197  uvtx01vtx  23222  wlkntrl  23283  0spth  23292  1pthonlem1  23310  2pthlem1  23316  3v3e3cycl1  23352  constr3trllem1  23358  constr3pthlem3  23365  4cycl4v4e  23374  4cycl4dv  23375  0conngra  23382  ex-opab  23461  grpoinvf  23549  ismgm  23629  rngomndo  23730  nvmid  23867  nmlnoubi  24018  hiidrcl  24319  hsn0elch  24473  shjshseli  24718  cmbr4i  24826  dfiop2  24979  kbpj  25182  nmopun  25240  adjeq0  25317  kbass2  25343  pjssdif1i  25401  pjinvari  25417  pjcmul2i  25428  pj3i  25434  stge1i  25464  stle0i  25465  sumdmdlem2  25645  dmdbr6ati  25649  dmdbr7ati  25650  rabsnel  25710  disjdifprg  25742  ofoprabco  25805  fpwrelmapffslem  25856  xrlelttric  25869  iundisj2cnt  25905  nn0min  25912  xrge0tsmsbi  26106  pstmxmet  26177  xrge0iifcnv  26216  xrge0iif1  26221  qqhre  26299  esumcl  26339  esumpr2  26370  esumpinfval  26375  esumpcvgval  26380  ofcfn  26395  pwsiga  26426  prsiga  26427  sigainb  26432  measiuns  26484  relfae  26516  sitgf  26580  eulerpartgbij  26602  sgnmulsgn  26779  sgnmulsgp  26780  plymulx  26796  signswch  26809  signslema  26810  signstlen  26815  subfacp1lem5  26919  erdszelem8  26933  kur14lem1  26941  indispcon  26970  cvmsss2  27010  relexpsucr  27178  prodf1f  27253  fprodshft  27333  fprodrev  27334  dfpo2  27411  dfon2lem7  27448  wfrlem4  27573  wfrlem14  27583  frrlem6  27623  nosgnn0i  27646  nobndlem2  27680  nobndlem4  27682  nobndlem5  27683  nobndlem6  27684  brbigcup  27775  elsingles  27795  fnimage  27806  funpartlem  27819  dfrdg4  27827  imagesset  27830  altopthsn  27838  elaltxp  27852  ellines  28029  linethru  28030  rankeq1o  28055  elhf2  28059  hfninf  28070  limsucncmpi  28138  volsupnfl  28277  cnambfre  28281  dvasin  28321  dvacos  28322  nn0prpwlem  28358  fneref  28397  refref  28398  neibastop2lem  28422  sdclem2  28479  sstotbnd2  28514  ssbnd  28528  grpokerinj  28591  isdrngo1  28603  prtlem12  28854  elrfirn  28873  ismrcd1  28876  istopclsd  28878  rabren3dioph  28996  jm2.17b  29146  jm2.22  29186  jm2.23  29187  ttac  29227  pw2f1ocnv  29228  dnnumch1  29239  hbtlem5  29326  mncn0  29338  aaitgo  29361  rngunsnply  29372  ssrecnpr  29436  seff  29437  sblpnf  29438  dvconstbi  29450  ipo0  29547  ifr0  29548  addrfn  29570  subrfn  29571  mulvfn  29572  refsum2cnlem1  29601  stoweidlem26  29664  stoweidlem50  29688  stoweidlem57  29695  2ffzoeq  30057  hash2prv  30069  wrdlen1  30093  wlkcomp  30129  wwlkn0s  30182  clwlkcomp  30269  frgra0v  30428  frgra1v  30433  1vwmgra  30438  vdgfrgragt2  30463  frgrancvvdeqlem3  30468  frgrawopreg1  30486  frgrawopreg2  30487  2spot0  30500  zlmodzxzldeplem4  30751  bnj145OLD  31417  bnj216  31422  bnj151  31569  bnj517  31577  bnj970  31639  bnj1014  31652  bnj1145  31683  bnj1498  31751  bj-speiv  31849  bj-snglex  32046  bj-inftyexpidisj  32110  riotasv2d  32178  lkrscss  32313  islshpkrN  32335  isline  32953  ispointN  32956  0psubN  32963  linepsubN  32966  atpsubN  32967  cdlemk36  34127  diafn  34249  dibfna  34369  dibvalrel  34378  dicvalrelN  34400  diclspsn  34409  dihvalrel  34494  dih1  34501  lclkrlem1  34721  lclkr  34748  mapd1o  34863  mapdin  34877  hdmapfnN  35047  hgmapfnN  35106
  Copyright terms: Public domain W3C validator