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

Theorem mpbiri 226
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 225 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  dedt  925  spei  1967  nfald2  2065  nfabd2  2592  dedhb  3106  sbceqal  3214  ssdifeq0  3712  r19.2zb  3720  dedth  3782  pwidg  3813  elpr2  3835  snidg  3841  exsnrex  3850  ifpr  3858  prid1g  3912  pwpw0  3948  sssn  3959  preqr1  3974  pwsnALT  4012  unimax  4051  intmin3  4080  syl6eqbr  4252  intabs  4364  pwnss  4368  0inp0  4374  copsexg  4445  euotd  4460  elopab  4465  epelg  4498  ord0eln0  4638  sucidg  4662  nsuceq0  4664  onun2i  4700  fr3nr  4763  onprc  4768  ordeleqon  4772  onint0  4779  0elsuc  4818  onuninsuci  4823  orduninsuc  4826  ordzsl  4828  onzsl  4829  tfinds  4842  limomss  4853  limom  4863  peano5  4871  elvvuni  4941  posn  4949  frsn  4951  eqrelriv  4972  relopabi  5003  opabid2  5007  ididg  5029  iss  5192  xpexr  5310  funopg  5488  fn0  5567  f00  5631  f1o00  5713  fo00  5714  brprcneu  5724  dffn5  5775  fsn  5909  fconstfv  5957  eufnfv  5975  f1eqcocnv  6031  oprabid  6108  elrnmpt2  6186  ov6g  6214  ovelrn  6225  caovmo  6287  offn  6319  caofinvl  6334  eqop2  6393  1stconst  6438  2ndconst  6439  dftpos3  6500  dftpos4  6501  nfriotad  6561  riotaprop  6576  riotasvdOLD  6596  riotasv2d  6597  riotasv2dOLD  6598  riotasv3dOLD  6602  oawordeulem  6800  omwordi  6817  nnmwordi  6881  riiner  6980  ecopover  7011  map0g  7056  mapsn  7058  elixpsn  7104  en0  7173  en1  7177  fiprc  7191  sbthlem2  7221  sbthlem4  7223  sbthlem5  7224  nneneq  7293  sdom1  7311  fineqvlem  7326  nfielex  7340  findcard  7350  findcard2  7351  elfiun  7438  marypha1lem  7441  oicl  7501  oif  7502  oion  7508  hartogslem1  7514  hartogs  7516  card2on  7525  0wdom  7541  brwdom2  7544  sucprcreg  7570  inf3lem6  7591  noinfepOLD  7618  cantnflem3  7650  cantnflem4  7651  wemapwe  7657  cnfcom  7660  tctr  7682  r1tr  7705  r1rankidb  7733  r1pw  7774  scottex  7814  scott0  7815  bnd2  7822  tskwe  7842  oncard  7852  cardlim  7864  harsdom  7887  dfac8alem  7915  cardaleph  7975  iunfictbso  8000  infmap2  8103  ackbij1lem18  8122  cff  8133  cfsuc  8142  cff1  8143  cflim2  8148  cfss  8150  sdom2en01  8187  infpssrlem4  8191  fin23lem7  8201  fin23lem11  8202  isfin2-2  8204  fin23lem26  8210  fin23lem19  8221  fin23lem17  8223  isf34lem2  8258  isf34lem4  8262  fin1a2lem6  8290  fin1a2lem10  8294  fin1a2lem12  8296  itunifn  8302  hsmexlem1  8311  axcc2lem  8321  dcomex  8332  axdc3lem4  8338  ondomon  8443  konigthlem  8448  pwcfsdom  8463  cfpwsdom  8464  axpowndlem3  8479  canth4  8527  canthnumlem  8528  canthwelem  8530  canthwe  8531  canthp1lem2  8533  pwfseqlem4  8542  pwfseqlem5  8543  gchaleph  8551  gch2  8555  winainflem  8573  0tsk  8635  rankcf  8657  tskcard  8661  gruina  8698  grutsk  8702  tskmid  8720  indpi  8789  nqereu  8811  mulcanenq  8842  recmulnq  8846  archnq  8862  ltsopr  8914  1ne0sr  8976  0idsr  8977  00sr  8979  leid  9174  lelttric  9185  divcan3  9707  lemul1a  9869  nn1suc  10026  nn0n0n1ge2b  10286  nn0ind-raph  10375  elnn1uz2  10557  indstr2  10559  uzsupss  10573  rpnnen1lem4  10608  rpnnen1lem5  10609  xrnemnf  10723  xrnepnf  10724  mnfltxr  10729  nn0pnfge0  10733  xrlttri  10737  xrlttr  10738  xrleid  10748  qbtwnxr  10791  xmullem2  10849  xlemul1a  10872  xrub  10895  ixxun  10937  fztpval  11112  fseq1p1m1  11127  elfznelfzob  11198  ltweuz  11306  fzfi  11316  ser0f  11381  0exp  11420  faclbnd4lem1  11589  bcn1  11609  hashnemnf  11633  hashv01gt1  11634  hashle00  11674  hashgt12el2  11688  hashmap  11703  hashpw  11704  hashf1  11711  fz1isolem  11715  swrdlen  11775  cats1un  11795  wrdind  11796  sqr0lem  12051  sqrsq  12080  fsumrev  12567  fsumshft  12568  egt2lt3  12810  0dvds  12875  bitsp1o  12950  gcddvds  13020  bezout  13047  1nprm  13089  prmind2  13095  rpdvds  13129  pcpre1  13221  vdwapf  13345  vdwapid1  13348  ram0  13395  ramz  13398  prmlem0  13433  strle1  13565  restsspw  13664  prdsdsfn  13692  imasdsfn  13745  imasaddfnlem  13758  imasvscafn  13767  xpscfv  13792  xpsfrnel  13793  isacs1i  13887  cidfn  13909  comffn  13936  isoval  13995  sscres  14028  cofucl  14090  idffth  14135  ressffth  14140  catcoppccl  14268  1stfcl  14299  2ndfcl  14300  prfcl  14305  evlfcl  14324  curf1cl  14330  curfcl  14334  hofcl  14361  yonedainv  14383  pospo  14435  ipopos  14591  acsficl2d  14607  dirref  14685  mgmidcl  14716  mgmlrid  14717  symggrp  15108  symgid  15109  cntzssv  15132  slwpgp  15252  frgpmhm  15402  frgpuptinv  15408  frgpup3lem  15414  gsumcom2  15554  abv0  15924  psrvscafval  16459  psrridm  16473  ltbwe  16538  psrbag0  16559  psrbagsn  16560  subrgascl  16563  zrhrhm  16798  baspartn  17024  eltg3  17032  fctop  17073  cctop  17075  discld  17158  mretopd  17161  neipeltop  17198  neitr  17249  restcls  17250  ordtbaslem  17257  ordtuni  17259  idcn  17326  cnrmi  17429  cmpsublem  17467  cmpsub  17468  tgcmp  17469  uncmp  17471  hauscmplem  17474  cmpfi  17476  bwth  17478  1stcrestlem  17520  disllycmp  17566  dis1stc  17567  kgeni  17574  1stckgenlem  17590  kqffn  17762  snfil  17901  filcon  17920  cfinfil  17930  ufileu  17956  filufint  17957  fixufil  17959  cfinufil  17965  ufilen  17967  fin1aufil  17969  fmf  17982  rnelfm  17990  flimclslem  18021  hauspwpwf1  18024  supnfcls  18057  flimfnfcls  18065  fclscmp  18067  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALT  18087  ptcmplem1  18088  cnextrel  18099  tsmsfbas  18162  ustref  18253  trust  18264  restutop  18272  isusp  18296  xmet0  18377  imasdsf1olem  18408  blfvalps  18418  blfps  18441  blf  18442  restmetu  18622  dscmet  18625  isngp2  18649  nm0  18678  nrginvrcn  18732  nmoix  18768  qdensere  18809  iccconn  18866  iccpnfcnv  18974  xrhmeo  18976  lebnumlem3  18993  cmetss  19272  bcthlem5  19286  minveclem3b  19334  cniccbdd  19363  ovolicc2lem4  19421  iunmbl  19452  ioorinv  19473  ioorcl  19474  i1f1lem  19584  limcvallem  19763  ellimc2  19769  limccnp  19783  limccnp2  19784  limcco  19785  perfdvf  19795  recnprss  19796  fncpn  19824  dvcmulf  19836  c1lip1  19886  lhop2  19904  q1pcl  20083  r1pdeglt  20086  ply1remlem  20090  plyssc  20124  ulm0  20312  cxpeq0  20574  cxplea  20592  asinlem  20713  isppw2  20903  muval2  20922  dchrfi  21044  dchrpt  21056  bposlem6  21078  lgsdir2lem2  21113  lgsqr  21135  2sqlem7  21159  2sqlem11  21164  chtppilim  21174  uhgra0  21349  uhgra0v  21350  umgra0  21365  usgra0  21395  usgra0v  21396  usgraedg4  21411  usgra1v  21414  nb3graprlem1  21465  cusgra1v  21475  cusgraexilem2  21481  uvtx01vtx  21506  wlkntrl  21567  0spth  21576  1pthonlem1  21594  2pthlem1  21600  3v3e3cycl1  21636  constr3trllem1  21642  constr3pthlem3  21649  4cycl4v4e  21658  4cycl4dv  21659  0conngra  21666  ex-opab  21745  grpoinvf  21833  ismgm  21913  rngomndo  22014  nvmid  22151  nmlnoubi  22302  hiidrcl  22602  hsn0elch  22755  shjshseli  23000  cmbr4i  23108  dfiop2  23261  kbpj  23464  nmopun  23522  adjeq0  23599  kbass2  23625  pjssdif1i  23683  pjinvari  23699  pjcmul2i  23710  pj3i  23716  stge1i  23746  stle0i  23747  sumdmdlem2  23927  dmdbr6ati  23931  dmdbr7ati  23932  disjdifprg  24022  ofoprabco  24084  xrlelttric  24123  iundisj2cnt  24160  xrge0tsmsbi  24229  pstmxmet  24297  xrge0iifcnv  24324  xrge0iif1  24329  qqhre  24391  esumcl  24432  esumpr2  24463  esumpinfval  24468  esumpcvgval  24473  ofcfn  24488  pwsiga  24518  prsiga  24519  sigainb  24524  measiuns  24576  relfae  24603  sitgf  24665  subfacp1lem5  24875  erdszelem8  24889  kur14lem1  24897  indispcon  24926  cvmsss2  24966  relexpsucr  25135  prodf1f  25225  fprodshft  25305  fprodrev  25306  dfpo2  25383  dfon2lem7  25421  wfrlem4  25546  wfrlem14  25556  frrlem6  25596  nosgnn0i  25619  nobndlem2  25653  nobndlem4  25655  nobndlem5  25656  nobndlem6  25657  brbigcup  25748  elsingles  25768  fnimage  25779  funpartlem  25792  dfrdg4  25800  imagesset  25803  altopthsn  25811  elaltxp  25825  axcgrtr  25859  axsegconlem9  25869  axlowdimlem5  25890  axlowdimlem17  25902  axlowdim1  25903  ellines  26091  linethru  26092  rankeq1o  26117  elhf2  26121  hfninf  26132  limsucncmpi  26200  volsupnfl  26263  cnambfre  26267  dvreasin  26304  nn0prpwlem  26339  fneref  26378  refref  26379  neibastop2lem  26403  sdclem2  26460  sstotbnd2  26497  ssbnd  26511  grpokerinj  26574  isdrngo1  26586  prtlem12  26730  elrfirn  26763  ismrcd1  26766  istopclsd  26768  rabren3dioph  26890  jm2.17b  27040  jm2.22  27080  jm2.23  27081  ttac  27121  pw2f1ocnv  27122  dnnumch1  27133  ellspd  27245  hbtlem5  27323  mncn0  27335  aaitgo  27358  rngunsnply  27369  en2eleq  27372  pmtrfmvdn0  27394  symggen  27402  psgnunilem1  27407  ssrecnpr  27528  seff  27529  sblpnf  27530  dvconstbi  27542  ipo0  27642  ifr0  27643  addrfn  27667  subrfn  27668  mulvfn  27669  refsum2cnlem1  27698  stoweidlem26  27765  stoweidlem50  27789  stoweidlem57  27796  f0bi  28092  oprabv  28103  2ffzoeq  28163  hash2prv  28193  ccatvalfn  28210  swrdvalfn  28220  swrdccatin1  28239  cshw1  28309  wlkcomp  28339  frgra0v  28457  frgra1v  28462  1vwmgra  28467  vdgfrgragt2  28492  frgrancvvdeqlem3  28495  frgrawopreg1  28513  frgrawopreg2  28514  2spot0  28527  bnj145  29168  bnj216  29173  bnj151  29322  bnj517  29330  bnj970  29392  bnj1014  29405  bnj1145  29436  bnj1498  29504  nfald2OLD7  29791  lkrscss  29970  islshpkrN  29992  isline  30610  ispointN  30613  0psubN  30620  linepsubN  30623  atpsubN  30624  cdlemk36  31784  diafn  31906  dibfna  32026  dibvalrel  32035  dicvalrelN  32057  diclspsn  32066  dihvalrel  32151  dih1  32158  lclkrlem1  32378  lclkr  32405  mapd1o  32520  mapdin  32534  hdmapfnN  32704  hgmapfnN  32763
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 179
  Copyright terms: Public domain W3C validator