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  948  spei  1965  nfald2  2030  nfabd2  2633  dedhb  3226  sbceqal  3340  sbcel12  3773  ssdifeq0  3859  r19.2zb  3868  dedth  3939  pwidg  3971  elpr2  3994  snidg  4001  exsnrex  4012  ifpr  4022  rabrsn  4043  prid1g  4079  pwpw0  4119  sssn  4129  preqr1  4144  pwsnALT  4184  unimax  4225  intmin3  4254  syl6eqbr  4427  intabs  4551  pwnss  4555  0inp0  4562  copsexg  4674  copsexgOLD  4675  euotd  4690  elopab  4695  epelg  4731  ord0eln0  4871  sucidg  4895  nsuceq0  4897  onun2i  4932  elvvuni  4997  posn  5005  frsn  5007  eqrelriv  5031  relopabi  5063  opabid2  5067  ididg  5091  iss  5252  funopg  5548  fn0  5628  f00  5691  f0bi  5692  f1o00  5771  fo00  5772  brprcneu  5782  dffn5  5836  fsn  5980  fnsnb  5997  fconstfv  6039  eufnfv  6050  f1eqcocnv  6098  nfriotad  6159  riotaprop  6175  oprabid  6214  elrnmpt2  6303  ov6g  6328  ovelrn  6339  caovmo  6400  offn  6431  caofinvl  6447  fr3nr  6491  onprc  6496  ordeleqon  6500  onint0  6507  0elsuc  6546  onuninsuci  6551  orduninsuc  6554  ordzsl  6556  onzsl  6557  tfinds  6570  limomss  6581  limom  6591  peano5  6599  xpexr  6618  eqop2  6717  1stconst  6761  2ndconst  6762  funsssuppss  6815  dftpos3  6863  dftpos4  6864  oawordeulem  7093  omwordi  7110  nnmwordi  7174  riiner  7273  ecopover  7304  map0g  7352  mapsn  7354  elixpsn  7402  en0  7472  en1  7476  fiprc  7491  sbthlem2  7522  sbthlem4  7524  sbthlem5  7525  nneneq  7594  sdom1  7613  fineqvlem  7628  nfielex  7642  findcard  7652  findcard2  7653  elfiun  7781  marypha1lem  7784  oicl  7844  oif  7845  oion  7851  hartogslem1  7857  hartogs  7859  wemapso2  7869  card2on  7870  0wdom  7886  brwdom2  7889  sucprcregOLD  7916  inf3lem6  7940  noinfepOLD  7967  cantnflem3  8000  cantnflem4  8001  cantnflem3OLD  8022  cantnflem4OLD  8023  wemapwe  8029  wemapweOLD  8030  cnfcom  8034  cnfcomOLD  8042  tctr  8061  r1tr  8084  r1rankidb  8112  r1pw  8153  scottex  8193  scott0  8194  bnd2  8201  tskwe  8221  oncard  8231  cardlim  8243  harsdom  8266  en2eleq  8276  dfac8alem  8300  cardaleph  8360  iunfictbso  8385  infmap2  8488  ackbij1lem18  8507  cff  8518  cfsuc  8527  cff1  8528  cflim2  8533  cfss  8535  sdom2en01  8572  infpssrlem4  8576  fin23lem7  8586  fin23lem11  8587  isfin2-2  8589  fin23lem26  8595  fin23lem19  8606  fin23lem17  8608  isf34lem2  8643  isf34lem4  8647  fin1a2lem6  8675  fin1a2lem10  8679  fin1a2lem12  8681  itunifn  8687  hsmexlem1  8696  axcc2lem  8706  dcomex  8717  axdc3lem4  8723  ondomon  8828  konigthlem  8833  pwcfsdom  8848  cfpwsdom  8849  axpowndlem3  8865  axpowndlem3OLD  8866  canth4  8915  canthnumlem  8916  canthwelem  8918  canthwe  8919  canthp1lem2  8921  pwfseqlem4  8930  pwfseqlem5  8931  gchaleph  8939  gch2  8943  winainflem  8961  0tsk  9023  rankcf  9045  tskcard  9049  gruina  9086  grutsk  9090  tskmid  9108  indpi  9177  nqereu  9199  mulcanenq  9230  recmulnq  9234  archnq  9250  ltsopr  9302  1ne0sr  9364  0idsr  9365  00sr  9367  leid  9571  lelttric  9582  divcan3  10119  lemul1a  10284  nn1suc  10444  nn0n0n1ge2b  10745  nn0ind-raph  10843  elnn1uz2  11032  indstr2  11034  uzsupss  11048  rpnnen1lem4  11083  rpnnen1lem5  11084  xrnemnf  11200  xrnepnf  11201  mnfltxr  11208  nn0pnfge0  11213  xrlttri  11217  xrlttr  11218  xrleid  11228  qbtwnxr  11271  xmullem2  11329  xlemul1a  11352  xrub  11375  ixxun  11417  fztpval  11619  fseq1p1m1  11635  elfznelfzob  11732  ltweuz  11885  fzfi  11895  ser0f  11960  0exp  12000  faclbnd4lem1  12170  bcn1  12190  hashnemnf  12216  hashv01gt1  12217  hashle00  12260  hashgt12el2  12276  hash2prd  12283  hashmap  12299  hashpw  12300  hashf1  12312  fz1isolem  12316  0wrd0  12355  ccatvalfn  12382  swrdlen  12421  swrdvalfn  12434  swrdspsleq  12444  cats1un  12472  wrdind  12473  wrd2ind  12474  swrdccatin1  12476  repswsymballbi  12520  cshw1  12558  sqr0lem  12832  sqrsq  12861  mptfzshft  13347  fsumrev  13348  egt2lt3  13590  0dvds  13655  bitsp1o  13731  gcddvds  13801  bezout  13828  1nprm  13870  prmind2  13876  rpdvds  13912  pcpre1  14011  vdwapf  14135  vdwapid1  14138  ram0  14185  ramz  14188  cshws0  14230  prmlem0  14235  strle1  14371  restsspw  14472  prdsdsfn  14505  imasdsfn  14554  imasaddfnlem  14568  imasvscafn  14577  xpscfv  14602  xpsfrnel  14603  isacs1i  14697  cidfn  14719  comffn  14746  isoval  14805  sscres  14838  cofucl  14900  idffth  14945  ressffth  14950  catcoppccl  15078  1stfcl  15109  2ndfcl  15110  prfcl  15115  evlfcl  15134  curf1cl  15140  curfcl  15144  hofcl  15171  yonedainv  15193  pospo  15245  lubfun  15252  glbfun  15265  joindmss  15279  meetdmss  15293  ipopos  15432  acsficl2d  15448  dirref  15507  mgmidcl  15538  mgmlrid  15539  cntzssv  15948  symggrp  16007  symgid  16008  idresperm  16016  pmtrfmvdn0  16070  symggen  16078  psgnunilem1  16101  psgnprfval  16129  slwpgp  16216  frgpmhm  16366  frgpuptinv  16372  frgpup3lem  16378  gsumcom2  16572  abv0  17022  rrgsupp  17468  psrvscafval  17567  psrridm  17582  psrridmOLD  17583  ltbwe  17661  psrbag0  17683  psrbagsn  17684  subrgascl  17687  zrhrhm  18052  psgnodpmr  18129  frlmphl  18315  ellspd  18339  ellspdOLD  18340  mattpostpos  18449  mavmul0  18474  mavmul0g  18475  mdet0f1o  18515  m1detdiag  18519  m2detleiblem5  18547  m2detleiblem6  18548  m2detleiblem3  18551  m2detleiblem4  18552  maducoeval2  18562  baspartn  18675  eltg3  18683  fctop  18724  cctop  18726  discld  18809  mretopd  18812  neipeltop  18849  neitr  18900  restcls  18901  ordtbaslem  18908  ordtuni  18910  idcn  18977  cnrmi  19080  cmpsublem  19118  cmpsub  19119  tgcmp  19120  uncmp  19122  hauscmplem  19125  cmpfi  19127  bwth  19129  bwthOLD  19130  1stcrestlem  19172  disllycmp  19218  dis1stc  19219  kgeni  19226  1stckgenlem  19242  kqffn  19414  snfil  19553  filcon  19572  cfinfil  19582  ufileu  19608  filufint  19609  fixufil  19611  cfinufil  19617  ufilen  19619  fin1aufil  19621  fmf  19634  rnelfm  19642  flimclslem  19673  hauspwpwf1  19676  supnfcls  19709  flimfnfcls  19717  fclscmp  19719  alexsubALTlem2  19736  alexsubALTlem3  19737  alexsubALT  19739  ptcmplem1  19740  cnextrel  19751  tsmsfbas  19814  ustref  19909  trust  19920  restutop  19928  isusp  19952  xmet0  20033  imasdsf1olem  20064  blfvalps  20074  blfps  20097  blf  20098  restmetu  20278  dscmet  20281  isngp2  20305  nm0  20334  nrginvrcn  20388  nmoix  20424  qdensere  20465  iccconn  20523  iccpnfcnv  20632  xrhmeo  20634  lebnumlem3  20651  cmetss  20941  bcthlem5  20955  rrxmfval  21021  minveclem3b  21031  cniccbdd  21061  ovolicc2lem4  21119  iunmbl  21150  ioorinv  21172  ioorcl  21173  i1f1lem  21283  limcvallem  21462  ellimc2  21468  limccnp  21482  limccnp2  21483  limcco  21484  perfdvf  21494  recnprss  21495  fncpn  21523  dvcmulf  21535  c1lip1  21585  lhop2  21603  q1pcl  21743  r1pdeglt  21746  ply1remlem  21750  plyssc  21784  ulm0  21972  cxpeq0  22239  cxplea  22257  asinlem  22379  isppw2  22569  muval2  22588  dchrfi  22710  dchrpt  22722  bposlem6  22744  lgsdir2lem2  22779  lgsqr  22801  2sqlem7  22825  2sqlem11  22830  chtppilim  22840  tgldimor  23073  tglnfn  23100  tglnunirn  23101  mircinv  23197  xmstrkgc  23267  axcgrtr  23296  axsegconlem9  23306  axlowdimlem5  23327  axlowdimlem17  23339  axlowdim1  23340  uhgra0  23378  uhgra0v  23379  umgra0  23394  usgra0  23424  usgra0v  23425  usgraedg4  23440  usgra1v  23443  nb3graprlem1  23494  cusgra1v  23504  cusgraexilem2  23510  uvtx01vtx  23535  wlkntrl  23596  0spth  23605  1pthonlem1  23623  2pthlem1  23629  3v3e3cycl1  23665  constr3trllem1  23671  constr3pthlem3  23678  4cycl4v4e  23687  4cycl4dv  23688  0conngra  23695  ex-opab  23774  grpoinvf  23862  ismgm  23942  rngomndo  24043  nvmid  24180  nmlnoubi  24331  hiidrcl  24632  hsn0elch  24786  shjshseli  25031  cmbr4i  25139  dfiop2  25292  kbpj  25495  nmopun  25553  adjeq0  25630  kbass2  25656  pjssdif1i  25714  pjinvari  25730  pjcmul2i  25741  pj3i  25747  stge1i  25777  stle0i  25778  sumdmdlem2  25958  dmdbr6ati  25962  dmdbr7ati  25963  rabsnel  26022  disjdifprg  26053  ofoprabco  26116  fpwrelmapffslem  26166  xrlelttric  26179  iundisj2cnt  26217  nn0min  26224  xrge0tsmsbi  26388  pstmxmet  26458  xrge0iifcnv  26497  xrge0iif1  26502  qqhre  26580  esumcl  26620  esumpr2  26651  esumpinfval  26656  esumpcvgval  26661  ofcfn  26676  pwsiga  26707  prsiga  26708  sigainb  26713  measiuns  26765  relfae  26797  sitgf  26867  eulerpartgbij  26889  sgnmulsgn  27066  sgnmulsgp  27067  plymulx  27083  signswch  27096  signslema  27097  signstlen  27102  subfacp1lem5  27206  erdszelem8  27220  kur14lem1  27228  indispcon  27257  cvmsss2  27297  relexpsucr  27466  prodf1f  27541  fprodshft  27621  fprodrev  27622  dfpo2  27699  dfon2lem7  27736  wfrlem4  27861  wfrlem14  27871  frrlem6  27911  nosgnn0i  27934  nobndlem2  27968  nobndlem4  27970  nobndlem5  27971  nobndlem6  27972  brbigcup  28063  elsingles  28083  fnimage  28094  funpartlem  28107  dfrdg4  28115  imagesset  28118  altopthsn  28126  elaltxp  28140  ellines  28317  linethru  28318  rankeq1o  28343  elhf2  28347  hfninf  28358  limsucncmpi  28425  volsupnfl  28574  cnambfre  28578  dvasin  28618  dvacos  28619  nn0prpwlem  28655  fneref  28694  refref  28695  neibastop2lem  28719  sdclem2  28776  sstotbnd2  28811  ssbnd  28825  grpokerinj  28888  isdrngo1  28900  ac6s6  29122  prtlem12  29150  elrfirn  29169  ismrcd1  29172  istopclsd  29174  rabren3dioph  29292  jm2.17b  29442  jm2.22  29482  jm2.23  29483  ttac  29523  pw2f1ocnv  29524  dnnumch1  29535  hbtlem5  29622  mncn0  29634  aaitgo  29657  rngunsnply  29668  ssrecnpr  29732  seff  29733  sblpnf  29734  dvconstbi  29746  ipo0  29843  ifr0  29844  addrfn  29866  subrfn  29867  mulvfn  29868  refsum2cnlem1  29897  stoweidlem26  29959  stoweidlem50  29983  stoweidlem57  29990  2ffzoeq  30352  hash2prv  30364  wrdlen1  30388  wlkcomp  30424  wwlkn0s  30477  clwlkcomp  30564  frgra0v  30723  frgra1v  30728  1vwmgra  30733  vdgfrgragt2  30758  frgrancvvdeqlem3  30763  frgrawopreg1  30781  frgrawopreg2  30782  2spot0  30795  fsuppmapnn0fiubex  30938  zlmodzxzldeplem4  31152  d1mat2pmat  31202  cpmat1dlem  31289  cpmat1d  31290  bnj145OLD  32018  bnj216  32023  bnj151  32170  bnj517  32178  bnj970  32240  bnj1014  32253  bnj1145  32284  bnj1498  32352  bj-dedthm  32397  bj-speiv  32521  bj-exlimmpbir  32714  bj-snglex  32766  bj-inftyexpidisj  32839  riotasv2d  32914  lkrscss  33049  islshpkrN  33071  isline  33689  ispointN  33692  0psubN  33699  linepsubN  33702  atpsubN  33703  cdlemk36  34863  diafn  34985  dibfna  35105  dibvalrel  35114  dicvalrelN  35136  diclspsn  35145  dihvalrel  35230  dih1  35237  lclkrlem1  35457  lclkr  35484  mapd1o  35599  mapdin  35613  hdmapfnN  35783  hgmapfnN  35842
  Copyright terms: Public domain W3C validator