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

Theorem mpbiri 225
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 224 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  dedt  924  spei  1966  nfald2  2060  nfabd2  2589  dedhb  3096  sbceqal  3204  ssdifeq0  3702  r19.2zb  3710  dedth  3772  pwidg  3803  elpr2  3825  snidg  3831  exsnrex  3840  ifpr  3848  prid1g  3902  pwpw0  3938  sssn  3949  preqr1  3964  pwsnALT  4002  unimax  4041  intmin3  4070  syl6eqbr  4241  intabs  4353  pwnss  4357  0inp0  4363  copsexg  4434  euotd  4449  elopab  4454  epelg  4487  ord0eln0  4627  sucidg  4651  nsuceq0  4653  onun2i  4689  fr3nr  4752  onprc  4757  ordeleqon  4761  onint0  4768  0elsuc  4807  onuninsuci  4812  orduninsuc  4815  ordzsl  4817  onzsl  4818  tfinds  4831  limomss  4842  limom  4852  peano5  4860  elvvuni  4930  posn  4938  frsn  4940  eqrelriv  4961  relopabi  4992  opabid2  4996  ididg  5018  iss  5181  xpexr  5299  funopg  5477  fn0  5556  f00  5620  f1o00  5702  fo00  5703  brprcneu  5713  dffn5  5764  fsn  5898  fconstfv  5946  eufnfv  5964  f1eqcocnv  6020  oprabid  6097  elrnmpt2  6175  ov6g  6203  ovelrn  6214  caovmo  6276  offn  6308  caofinvl  6323  eqop2  6382  1stconst  6427  2ndconst  6428  dftpos3  6489  dftpos4  6490  nfriotad  6550  riotaprop  6565  riotasvdOLD  6585  riotasv2d  6586  riotasv2dOLD  6587  riotasv3dOLD  6591  oawordeulem  6789  omwordi  6806  nnmwordi  6870  riiner  6969  ecopover  7000  map0g  7045  mapsn  7047  elixpsn  7093  en0  7162  en1  7166  fiprc  7180  sbthlem2  7210  sbthlem4  7212  sbthlem5  7213  nneneq  7282  sdom1  7300  fineqvlem  7315  nfielex  7329  findcard  7339  findcard2  7340  elfiun  7427  marypha1lem  7430  oicl  7490  oif  7491  oion  7497  hartogslem1  7503  hartogs  7505  card2on  7514  0wdom  7530  brwdom2  7533  sucprcreg  7559  inf3lem6  7580  noinfepOLD  7607  cantnflem3  7639  cantnflem4  7640  wemapwe  7646  cnfcom  7649  tctr  7671  r1tr  7694  r1rankidb  7722  r1pw  7763  scottex  7801  scott0  7802  bnd2  7809  tskwe  7829  oncard  7839  cardlim  7851  harsdom  7874  dfac8alem  7902  cardaleph  7962  iunfictbso  7987  infmap2  8090  ackbij1lem18  8109  cff  8120  cfsuc  8129  cff1  8130  cflim2  8135  cfss  8137  sdom2en01  8174  infpssrlem4  8178  fin23lem7  8188  fin23lem11  8189  isfin2-2  8191  fin23lem26  8197  fin23lem19  8208  fin23lem17  8210  isf34lem2  8245  isf34lem4  8249  fin1a2lem6  8277  fin1a2lem10  8281  fin1a2lem12  8283  itunifn  8289  hsmexlem1  8298  axcc2lem  8308  dcomex  8319  axdc3lem4  8325  ondomon  8430  konigthlem  8435  pwcfsdom  8450  cfpwsdom  8451  axpowndlem3  8466  canth4  8514  canthnumlem  8515  canthwelem  8517  canthwe  8518  canthp1lem2  8520  pwfseqlem4  8529  pwfseqlem5  8530  gchaleph  8542  gch2  8546  winainflem  8560  0tsk  8622  rankcf  8644  tskcard  8648  gruina  8685  grutsk  8689  tskmid  8707  indpi  8776  nqereu  8798  mulcanenq  8829  recmulnq  8833  archnq  8849  ltsopr  8901  1ne0sr  8963  0idsr  8964  00sr  8966  leid  9161  lelttric  9172  divcan3  9694  lemul1a  9856  nn1suc  10013  nn0n0n1ge2b  10273  nn0ind-raph  10362  elnn1uz2  10544  indstr2  10546  uzsupss  10560  rpnnen1lem4  10595  rpnnen1lem5  10596  xrnemnf  10710  xrnepnf  10711  mnfltxr  10716  nn0pnfge0  10720  xrlttri  10724  xrlttr  10725  xrleid  10735  qbtwnxr  10778  xmullem2  10836  xlemul1a  10859  xrub  10882  ixxun  10924  fztpval  11099  fseq1p1m1  11114  elfznelfzob  11185  ltweuz  11293  fzfi  11303  ser0f  11368  0exp  11407  faclbnd4lem1  11576  bcn1  11596  hashnemnf  11620  hashv01gt1  11621  hashle00  11661  hashgt12el2  11675  hashmap  11690  hashpw  11691  hashf1  11698  fz1isolem  11702  swrdlen  11762  cats1un  11782  wrdind  11783  sqr0lem  12038  sqrsq  12067  fsumrev  12554  fsumshft  12555  egt2lt3  12797  0dvds  12862  bitsp1o  12937  gcddvds  13007  bezout  13034  1nprm  13076  prmind2  13082  rpdvds  13116  pcpre1  13208  vdwapf  13332  vdwapid1  13335  ram0  13382  ramz  13385  prmlem0  13420  strle1  13552  restsspw  13651  prdsdsfn  13679  imasdsfn  13732  imasaddfnlem  13745  imasvscafn  13754  xpscfv  13779  xpsfrnel  13780  isacs1i  13874  cidfn  13896  comffn  13923  isoval  13982  sscres  14015  cofucl  14077  idffth  14122  ressffth  14127  catcoppccl  14255  1stfcl  14286  2ndfcl  14287  prfcl  14292  evlfcl  14311  curf1cl  14317  curfcl  14321  hofcl  14348  yonedainv  14370  pospo  14422  ipopos  14578  acsficl2d  14594  dirref  14672  mgmidcl  14703  mgmlrid  14704  symggrp  15095  symgid  15096  cntzssv  15119  slwpgp  15239  frgpmhm  15389  frgpuptinv  15395  frgpup3lem  15401  gsumcom2  15541  abv0  15911  psrvscafval  16446  psrridm  16460  ltbwe  16525  psrbag0  16546  psrbagsn  16547  subrgascl  16550  zrhrhm  16785  baspartn  17011  eltg3  17019  fctop  17060  cctop  17062  discld  17145  mretopd  17148  neipeltop  17185  neitr  17236  restcls  17237  ordtbaslem  17244  ordtuni  17246  idcn  17313  cnrmi  17416  cmpsublem  17454  cmpsub  17455  tgcmp  17456  uncmp  17458  hauscmplem  17461  cmpfi  17463  bwth  17465  1stcrestlem  17507  disllycmp  17553  dis1stc  17554  kgeni  17561  1stckgenlem  17577  kqffn  17749  snfil  17888  filcon  17907  cfinfil  17917  ufileu  17943  filufint  17944  fixufil  17946  cfinufil  17952  ufilen  17954  fin1aufil  17956  fmf  17969  rnelfm  17977  flimclslem  18008  hauspwpwf1  18011  supnfcls  18044  flimfnfcls  18052  fclscmp  18054  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALT  18074  ptcmplem1  18075  cnextrel  18086  tsmsfbas  18149  ustref  18240  trust  18251  restutop  18259  isusp  18283  xmet0  18364  imasdsf1olem  18395  blfvalps  18405  blfps  18428  blf  18429  restmetu  18609  dscmet  18612  isngp2  18636  nm0  18665  nrginvrcn  18719  nmoix  18755  qdensere  18796  iccconn  18853  iccpnfcnv  18961  xrhmeo  18963  lebnumlem3  18980  cmetss  19259  bcthlem5  19273  minveclem3b  19321  cniccbdd  19350  ovolicc2lem4  19408  iunmbl  19439  ioorinv  19460  ioorcl  19461  i1f1lem  19573  limcvallem  19750  ellimc2  19756  limccnp  19770  limccnp2  19771  limcco  19772  perfdvf  19782  recnprss  19783  fncpn  19811  dvcmulf  19823  c1lip1  19873  lhop2  19891  q1pcl  20070  r1pdeglt  20073  ply1remlem  20077  plyssc  20111  ulm0  20299  cxpeq0  20561  cxplea  20579  asinlem  20700  isppw2  20890  muval2  20909  dchrfi  21031  dchrpt  21043  bposlem6  21065  lgsdir2lem2  21100  lgsqr  21122  2sqlem7  21146  2sqlem11  21151  chtppilim  21161  uhgra0  21336  uhgra0v  21337  umgra0  21352  usgra0  21382  usgra0v  21383  usgraedg4  21398  usgra1v  21401  nb3graprlem1  21452  cusgra1v  21462  cusgraexilem2  21468  uvtx01vtx  21493  wlkntrl  21554  0spth  21563  1pthonlem1  21581  2pthlem1  21587  3v3e3cycl1  21623  constr3trllem1  21629  constr3pthlem3  21636  4cycl4v4e  21645  4cycl4dv  21646  0conngra  21653  ex-opab  21732  grpoinvf  21820  ismgm  21900  rngomndo  22001  nvmid  22138  nmlnoubi  22289  hiidrcl  22589  hsn0elch  22742  shjshseli  22987  cmbr4i  23095  dfiop2  23248  kbpj  23451  nmopun  23509  adjeq0  23586  kbass2  23612  pjssdif1i  23670  pjinvari  23686  pjcmul2i  23697  pj3i  23703  stge1i  23733  stle0i  23734  sumdmdlem2  23914  dmdbr6ati  23918  dmdbr7ati  23919  disjdifprg  24009  ofoprabco  24071  xrlelttric  24110  iundisj2cnt  24147  xrge0tsmsbi  24216  pstmxmet  24284  xrge0iifcnv  24311  xrge0iif1  24316  qqhre  24378  esumcl  24419  esumpr2  24450  esumpinfval  24455  esumpcvgval  24460  ofcfn  24475  pwsiga  24505  prsiga  24506  sigainb  24511  measiuns  24563  relfae  24590  sitgf  24652  subfacp1lem5  24862  erdszelem8  24876  kur14lem1  24884  indispcon  24913  cvmsss2  24953  relexpsucr  25122  prodf1f  25212  fprodshft  25292  fprodrev  25293  dfpo2  25370  dfon2lem7  25408  wfrlem4  25533  wfrlem14  25543  frrlem6  25583  nosgnn0i  25606  nobndlem2  25640  nobndlem4  25642  nobndlem5  25643  nobndlem6  25644  brbigcup  25735  elsingles  25755  fnimage  25766  funpartlem  25779  dfrdg4  25787  imagesset  25790  altopthsn  25798  elaltxp  25812  axcgrtr  25846  axsegconlem9  25856  axlowdimlem5  25877  axlowdimlem17  25889  axlowdim1  25890  ellines  26078  linethru  26079  rankeq1o  26104  elhf2  26108  hfninf  26119  limsucncmpi  26187  volsupnfl  26241  cnambfre  26245  dvreasin  26280  nn0prpwlem  26316  fneref  26355  refref  26356  neibastop2lem  26380  sdclem2  26437  sstotbnd2  26474  ssbnd  26488  grpokerinj  26551  isdrngo1  26563  prtlem12  26707  elrfirn  26740  ismrcd1  26743  istopclsd  26745  rabren3dioph  26867  jm2.17b  27017  jm2.22  27057  jm2.23  27058  ttac  27098  pw2f1ocnv  27099  dnnumch1  27110  ellspd  27222  hbtlem5  27300  mncn0  27312  aaitgo  27335  rngunsnply  27346  en2eleq  27349  pmtrfmvdn0  27371  symggen  27379  psgnunilem1  27384  ssrecnpr  27505  seff  27506  sblpnf  27507  dvconstbi  27519  ipo0  27619  ifr0  27620  addrfn  27644  subrfn  27645  mulvfn  27646  refsum2cnlem1  27675  stoweidlem26  27742  stoweidlem50  27766  stoweidlem57  27773  ccatvalfn  28151  swrdvalfn  28158  swrdccatin1  28171  cshw1  28238  frgra0v  28320  frgra1v  28325  1vwmgra  28330  vdgfrgragt2  28355  frgrancvvdeqlem3  28358  frgrawopreg1  28376  frgrawopreg2  28377  2spot0  28390  bnj145  29031  bnj216  29036  bnj151  29185  bnj517  29193  bnj970  29255  bnj1014  29268  bnj1145  29299  bnj1498  29367  nfald2OLD7  29654  lkrscss  29833  islshpkrN  29855  isline  30473  ispointN  30476  0psubN  30483  linepsubN  30486  atpsubN  30487  cdlemk36  31647  diafn  31769  dibfna  31889  dibvalrel  31898  dicvalrelN  31920  diclspsn  31929  dihvalrel  32014  dih1  32021  lclkrlem1  32241  lclkr  32268  mapd1o  32383  mapdin  32397  hdmapfnN  32567  hgmapfnN  32626
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator