MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbiri 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  nfald2  2029  nfabd2  2558  dedhb  3064  sbceqal  3172  ssdifeq0  3670  r19.2zb  3678  dedth  3740  pwidg  3771  elpr2  3793  snidg  3799  exsnrex  3808  ifpr  3816  prid1g  3870  pwpw0  3906  sssn  3917  preqr1  3932  pwsnALT  3970  unimax  4009  intmin3  4038  syl6eqbr  4209  intabs  4321  pwnss  4325  0inp0  4331  copsexg  4402  euotd  4417  elopab  4422  epelg  4455  ord0eln0  4595  sucidg  4619  nsuceq0  4621  onun2i  4656  fr3nr  4719  onprc  4724  ordeleqon  4728  onint0  4735  0elsuc  4774  onuninsuci  4779  orduninsuc  4782  ordzsl  4784  onzsl  4785  tfinds  4798  limomss  4809  limom  4819  peano5  4827  elvvuni  4897  posn  4905  frsn  4907  eqrelriv  4928  relopabi  4959  opabid2  4963  ididg  4985  iss  5148  xpexr  5266  funopg  5444  fn0  5523  f00  5587  f1o00  5669  fo00  5670  brprcneu  5680  dffn5  5731  fsn  5865  fconstfv  5913  eufnfv  5931  f1eqcocnv  5987  oprabid  6064  elrnmpt2  6142  ov6g  6170  ovelrn  6181  caovmo  6243  offn  6275  caofinvl  6290  eqop2  6349  1stconst  6394  2ndconst  6395  dftpos3  6456  dftpos4  6457  nfriotad  6517  riotaprop  6532  riotasvdOLD  6552  riotasv2d  6553  riotasv2dOLD  6554  riotasv3dOLD  6558  oawordeulem  6756  omwordi  6773  nnmwordi  6837  riiner  6936  ecopover  6967  map0g  7012  mapsn  7014  elixpsn  7060  en0  7129  en1  7133  fiprc  7147  sbthlem2  7177  sbthlem4  7179  sbthlem5  7180  nneneq  7249  sdom1  7267  fineqvlem  7282  nfielex  7296  findcard  7306  findcard2  7307  elfiun  7393  marypha1lem  7396  oicl  7454  oif  7455  oion  7461  hartogslem1  7467  hartogs  7469  card2on  7478  0wdom  7494  brwdom2  7497  sucprcreg  7523  inf3lem6  7544  noinfepOLD  7571  cantnflem3  7603  cantnflem4  7604  wemapwe  7610  cnfcom  7613  tctr  7635  r1tr  7658  r1rankidb  7686  r1pw  7727  scottex  7765  scott0  7766  bnd2  7773  tskwe  7793  oncard  7803  cardlim  7815  harsdom  7838  dfac8alem  7866  cardaleph  7926  iunfictbso  7951  infmap2  8054  ackbij1lem18  8073  cff  8084  cfsuc  8093  cff1  8094  cflim2  8099  cfss  8101  sdom2en01  8138  infpssrlem4  8142  fin23lem7  8152  fin23lem11  8153  isfin2-2  8155  fin23lem26  8161  fin23lem19  8172  fin23lem17  8174  isf34lem2  8209  isf34lem4  8213  fin1a2lem6  8241  fin1a2lem10  8245  fin1a2lem12  8247  itunifn  8253  hsmexlem1  8262  axcc2lem  8272  dcomex  8283  axdc3lem4  8289  ondomon  8394  konigthlem  8399  pwcfsdom  8414  cfpwsdom  8415  axpowndlem3  8430  canth4  8478  canthnumlem  8479  canthwelem  8481  canthwe  8482  canthp1lem2  8484  pwfseqlem4  8493  pwfseqlem5  8494  gchaleph  8506  gch2  8510  winainflem  8524  0tsk  8586  rankcf  8608  tskcard  8612  gruina  8649  grutsk  8653  tskmid  8671  indpi  8740  nqereu  8762  mulcanenq  8793  recmulnq  8797  archnq  8813  ltsopr  8865  1ne0sr  8927  0idsr  8928  00sr  8930  leid  9125  lelttric  9136  divcan3  9658  lemul1a  9820  nn1suc  9977  nn0n0n1ge2b  10237  nn0ind-raph  10326  elnn1uz2  10508  indstr2  10510  uzsupss  10524  rpnnen1lem4  10559  rpnnen1lem5  10560  xrnemnf  10674  xrnepnf  10675  mnfltxr  10680  nn0pnfge0  10684  xrlttri  10688  xrlttr  10689  xrleid  10699  qbtwnxr  10742  xmullem2  10800  xlemul1a  10823  xrub  10846  ixxun  10888  fztpval  11063  fseq1p1m1  11077  elfznelfzob  11148  ltweuz  11256  fzfi  11266  ser0f  11331  0exp  11370  faclbnd4lem1  11539  bcn1  11559  hashnemnf  11583  hashv01gt1  11584  hashle00  11624  hashgt12el2  11638  hashmap  11653  hashpw  11654  hashf1  11661  fz1isolem  11665  swrdlen  11725  cats1un  11745  wrdind  11746  sqr0lem  12001  sqrsq  12030  fsumrev  12517  fsumshft  12518  egt2lt3  12760  0dvds  12825  bitsp1o  12900  gcddvds  12970  bezout  12997  1nprm  13039  prmind2  13045  rpdvds  13079  pcpre1  13171  vdwapf  13295  vdwapid1  13298  ram0  13345  ramz  13348  prmlem0  13383  strle1  13515  restsspw  13614  prdsdsfn  13642  imasdsfn  13695  imasaddfnlem  13708  imasvscafn  13717  xpscfv  13742  xpsfrnel  13743  isacs1i  13837  cidfn  13859  comffn  13886  isoval  13945  sscres  13978  cofucl  14040  idffth  14085  ressffth  14090  catcoppccl  14218  1stfcl  14249  2ndfcl  14250  prfcl  14255  evlfcl  14274  curf1cl  14280  curfcl  14284  hofcl  14311  yonedainv  14333  pospo  14385  ipopos  14541  acsficl2d  14557  dirref  14635  mgmidcl  14666  mgmlrid  14667  symggrp  15058  symgid  15059  cntzssv  15082  slwpgp  15202  frgpmhm  15352  frgpuptinv  15358  frgpup3lem  15364  gsumcom2  15504  abv0  15874  psrvscafval  16409  psrridm  16423  ltbwe  16488  psrbag0  16509  psrbagsn  16510  subrgascl  16513  zrhrhm  16748  baspartn  16974  eltg3  16982  fctop  17023  cctop  17025  discld  17108  mretopd  17111  neipeltop  17148  neitr  17198  restcls  17199  ordtbaslem  17206  ordtuni  17208  idcn  17275  cnrmi  17378  cmpsublem  17416  cmpsub  17417  tgcmp  17418  uncmp  17420  hauscmplem  17423  cmpfi  17425  1stcrestlem  17468  disllycmp  17514  dis1stc  17515  kgeni  17522  1stckgenlem  17538  kqffn  17710  snfil  17849  filcon  17868  cfinfil  17878  ufileu  17904  filufint  17905  fixufil  17907  cfinufil  17913  ufilen  17915  fin1aufil  17917  fmf  17930  rnelfm  17938  flimclslem  17969  hauspwpwf1  17972  supnfcls  18005  flimfnfcls  18013  fclscmp  18015  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALT  18035  ptcmplem1  18036  cnextrel  18047  tsmsfbas  18110  ustref  18201  trust  18212  restutop  18220  isusp  18244  xmet0  18325  imasdsf1olem  18356  blfvalps  18366  blfps  18389  blf  18390  restmetu  18570  dscmet  18573  isngp2  18597  nm0  18626  nrginvrcn  18680  nmoix  18716  qdensere  18757  iccconn  18814  iccpnfcnv  18922  xrhmeo  18924  lebnumlem3  18941  cmetss  19220  bcthlem5  19234  minveclem3b  19282  cniccbdd  19311  ovolicc2lem4  19369  iunmbl  19400  ioorinv  19421  ioorcl  19422  i1f1lem  19534  limcvallem  19711  ellimc2  19717  limccnp  19731  limccnp2  19732  limcco  19733  perfdvf  19743  recnprss  19744  fncpn  19772  dvcmulf  19784  c1lip1  19834  lhop2  19852  q1pcl  20031  r1pdeglt  20034  ply1remlem  20038  plyssc  20072  ulm0  20260  cxpeq0  20522  cxplea  20540  asinlem  20661  isppw2  20851  muval2  20870  dchrfi  20992  dchrpt  21004  bposlem6  21026  lgsdir2lem2  21061  lgsqr  21083  2sqlem7  21107  2sqlem11  21112  chtppilim  21122  uhgra0  21297  uhgra0v  21298  umgra0  21313  usgra0  21343  usgra0v  21344  usgraedg4  21359  usgra1v  21362  nb3graprlem1  21413  cusgra1v  21423  cusgraexilem2  21429  uvtx01vtx  21454  wlkntrl  21515  0spth  21524  1pthonlem1  21542  2pthlem1  21548  3v3e3cycl1  21584  constr3trllem1  21590  constr3pthlem3  21597  4cycl4v4e  21606  4cycl4dv  21607  0conngra  21614  ex-opab  21693  grpoinvf  21781  ismgm  21861  rngomndo  21962  nvmid  22099  nmlnoubi  22250  hiidrcl  22550  hsn0elch  22703  shjshseli  22948  cmbr4i  23056  dfiop2  23209  kbpj  23412  nmopun  23470  adjeq0  23547  kbass2  23573  pjssdif1i  23631  pjinvari  23647  pjcmul2i  23658  pj3i  23664  stge1i  23694  stle0i  23695  sumdmdlem2  23875  dmdbr6ati  23879  dmdbr7ati  23880  disjdifprg  23970  ofoprabco  24032  xrlelttric  24071  iundisj2cnt  24108  xrge0tsmsbi  24177  pstmxmet  24245  xrge0iifcnv  24272  xrge0iif1  24277  qqhre  24339  esumcl  24380  esumpr2  24411  esumpinfval  24416  esumpcvgval  24421  ofcfn  24436  pwsiga  24466  prsiga  24467  sigainb  24472  measiuns  24524  relfae  24551  sitgf  24613  subfacp1lem5  24823  erdszelem8  24837  kur14lem1  24845  indispcon  24874  cvmsss2  24914  relexpsucr  25083  prodf1f  25173  fprodshft  25253  fprodrev  25254  dfpo2  25326  dfon2lem7  25359  wfrlem4  25473  wfrlem6  25475  wfrlem14  25483  frrlem6  25504  nosgnn0i  25527  nobndlem2  25561  nobndlem4  25563  nobndlem5  25564  nobndlem6  25565  brbigcup  25652  elsingles  25671  fnimage  25682  funpartlem  25695  dfrdg4  25703  altopthsn  25710  elaltxp  25724  axcgrtr  25758  axsegconlem9  25768  axlowdimlem5  25789  axlowdimlem17  25801  axlowdim1  25802  ellines  25990  linethru  25991  rankeq1o  26016  elhf2  26020  hfninf  26031  limsucncmpi  26099  volsupnfl  26150  cnambfre  26154  dvreasin  26179  nn0prpwlem  26215  fneref  26254  refref  26255  neibastop2lem  26279  sdclem2  26336  sstotbnd2  26373  ssbnd  26387  grpokerinj  26450  isdrngo1  26462  prtlem12  26606  elrfirn  26639  ismrcd1  26642  istopclsd  26644  rabren3dioph  26766  jm2.17b  26916  jm2.22  26956  jm2.23  26957  ttac  26997  pw2f1ocnv  26998  dnnumch1  27009  ellspd  27122  hbtlem5  27200  mncn0  27212  aaitgo  27235  rngunsnply  27246  en2eleq  27249  pmtrfmvdn0  27271  symggen  27279  psgnunilem1  27284  ssrecnpr  27405  seff  27406  sblpnf  27407  dvconstbi  27419  ipo0  27519  ifr0  27520  addrfn  27544  subrfn  27545  mulvfn  27546  refsum2cnlem1  27575  stoweidlem26  27642  stoweidlem50  27666  stoweidlem57  27673  swrdvalfn  28007  ccatvalfn  28008  swrdccatin1  28016  swrdccatin2  28018  frgra0v  28097  frgra1v  28102  1vwmgra  28107  vdgfrgragt2  28132  frgrancvvdeqlem3  28135  frgrawopreg1  28153  frgrawopreg2  28154  2spot0  28167  bnj145  28800  bnj216  28805  bnj151  28954  bnj517  28962  bnj970  29024  bnj1014  29037  bnj1145  29068  bnj1498  29136  nfald2OLD7  29401  lkrscss  29581  islshpkrN  29603  isline  30221  ispointN  30224  0psubN  30231  linepsubN  30234  atpsubN  30235  cdlemk36  31395  diafn  31517  dibfna  31637  dibvalrel  31646  dicvalrelN  31668  diclspsn  31677  dihvalrel  31762  dih1  31769  lclkrlem1  31989  lclkr  32016  mapd1o  32131  mapdin  32145  hdmapfnN  32315  hgmapfnN  32374
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