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  955  spei  2017  nfald2  2077  nfabd2  2637  dedhb  3266  sbceqal  3376  ssdifeq0  3898  r19.2zb  3907  dedth  3980  pwidg  4012  elpr2  4035  snidg  4042  exsnrex  4054  ifpr  4064  rabrsn  4086  prid1g  4122  pwpw0  4164  sssn  4174  preqr1  4190  pwsnALT  4230  unimax  4270  intmin3  4300  syl6eqbr  4476  intabs  4598  pwnss  4602  0inp0  4609  copsexg  4722  euotd  4737  elopab  4744  epelg  4781  ord0eln0  4921  sucidg  4945  nsuceq0  4947  onun2i  4982  elvvuni  5049  posn  5057  frsn  5059  eqrelriv  5084  relopabi  5116  opabid2  5121  ididg  5145  iss  5309  funopg  5602  fn0  5682  f00  5749  f0bi  5750  f1o00  5830  fo00  5831  brprcneu  5841  dffn5  5893  fsn  6045  fnsnb  6066  fconstfvOLD  6109  eufnfv  6121  f1eqcocnv  6179  nfriotad  6240  riotaprop  6255  oprabid  6297  elrnmpt2  6388  ov6g  6413  ovelrn  6424  caovmo  6485  offn  6524  caofinvl  6540  fr3nr  6588  onprc  6593  ordeleqon  6597  onint0  6604  0elsuc  6643  onuninsuci  6648  orduninsuc  6651  ordzsl  6653  onzsl  6654  tfinds  6667  limomss  6678  limom  6688  peano5  6696  xpexr  6713  eqop2  6814  1stconst  6861  2ndconst  6862  funsssuppss  6918  dftpos3  6965  dftpos4  6966  oawordeulem  7195  omwordi  7212  nnmwordi  7276  riiner  7376  ecopover  7407  map0g  7451  mapsn  7453  elixpsn  7501  en0  7571  en1  7575  fiprc  7590  sbthlem2  7621  sbthlem4  7623  sbthlem5  7624  nneneq  7693  sdom1  7712  fineqvlem  7727  nfielex  7741  findcard  7751  findcard2  7752  elfiun  7882  marypha1lem  7885  oicl  7946  oif  7947  oion  7953  hartogslem1  7959  hartogs  7961  wemapso2  7971  card2on  7972  0wdom  7988  brwdom2  7991  inf3lem6  8041  noinfepOLD  8068  cantnflem3  8101  cantnflem4  8102  cantnflem3OLD  8123  cantnflem4OLD  8124  wemapwe  8130  wemapweOLD  8131  cnfcom  8135  cnfcomOLD  8143  tctr  8162  r1tr  8185  r1rankidb  8213  r1pw  8254  scottex  8294  scott0  8295  bnd2  8302  tskwe  8322  oncard  8332  cardlim  8344  harsdom  8367  en2eleq  8377  dfac8alem  8401  cardaleph  8461  iunfictbso  8486  infmap2  8589  ackbij1lem18  8608  cff  8619  cfsuc  8628  cff1  8629  cflim2  8634  cfss  8636  sdom2en01  8673  infpssrlem4  8677  fin23lem7  8687  fin23lem11  8688  isfin2-2  8690  fin23lem26  8696  fin23lem19  8707  fin23lem17  8709  isf34lem2  8744  isf34lem4  8748  fin1a2lem6  8776  fin1a2lem10  8780  fin1a2lem12  8782  itunifn  8788  hsmexlem1  8797  axcc2lem  8807  dcomex  8818  axdc3lem4  8824  ondomon  8929  konigthlem  8934  pwcfsdom  8949  cfpwsdom  8950  axpowndlem3  8965  canth4  9014  canthnumlem  9015  canthwelem  9017  canthwe  9018  canthp1lem2  9020  pwfseqlem4  9029  pwfseqlem5  9030  gchaleph  9038  gch2  9042  winainflem  9060  0tsk  9122  rankcf  9144  tskcard  9148  gruina  9185  grutsk  9189  tskmid  9207  indpi  9274  nqereu  9296  mulcanenq  9327  recmulnq  9331  archnq  9347  ltsopr  9399  1ne0sr  9462  0idsr  9463  00sr  9465  leid  9669  lelttric  9680  divcan3  10227  lemul1a  10392  nn1suc  10552  nn0n0n1ge2b  10856  nn0lt10b  10921  nn0ind-raph  10960  elnn1uz2  11159  indstr2  11161  uzsupss  11175  rpnnen1lem4  11212  rpnnen1lem5  11213  xrnemnf  11331  xrnepnf  11332  mnfltxr  11339  nn0pnfge0  11344  xrlttri  11348  xrlttr  11349  xrleid  11359  qbtwnxr  11402  xmullem2  11460  xlemul1a  11483  xrub  11506  ixxun  11548  fztpval  11745  fseq1p1m1  11756  elfznelfzob  11897  ltweuz  12054  fzfi  12064  fsuppmapnn0fiubex  12080  ser0f  12142  0exp  12183  faclbnd4lem1  12353  bcn1  12373  hashnemnf  12399  hashv01gt1  12400  hashle00  12449  hashgt12el2  12466  hashmap  12477  hashpw  12478  hashf1  12490  fz1isolem  12494  hash2prd  12502  hash2prv  12509  0wrd0  12555  wrdlen1  12567  ccatvalfn  12588  swrdlen  12639  swrdspsleq  12665  cats1un  12692  wrdind  12693  wrd2ind  12694  swrdccatin1  12699  repswsymballbi  12743  cshw1  12781  scshwfzeqfzo  12785  trclfvcotr  12927  relexp1g  12943  relexp0rel  12952  relexprelg  12953  sqr0lem  13156  sqrtsq  13185  mptfzshft  13675  fsumrev  13676  prodf1f  13783  fprodrev  13863  egt2lt3  14021  0dvds  14088  bitsp1o  14167  gcddvds  14237  bezout  14264  1nprm  14306  prmind2  14312  rpdvds  14349  pcpre1  14450  vdwapf  14574  vdwapid1  14577  ram0  14624  ramz  14627  cshws0  14670  prmlem0  14675  strle1  14815  restsspw  14921  prdsdsfn  14954  imasdsfn  15003  imasaddfnlem  15017  imasvscafn  15026  xpscfv  15051  xpsfrnel  15052  isacs1i  15146  cidfn  15168  fnhomeqhomf  15179  comffn  15193  isoval  15253  sscres  15311  cofucl  15376  idffth  15421  ressffth  15426  catcoppccl  15586  estrchomfn  15603  funcestrcsetclem4  15611  funcestrcsetclem7  15614  equivestrcsetc  15620  funcsetcestrclem4  15626  funcsetcestrclem7  15629  1stfcl  15665  2ndfcl  15666  prfcl  15671  evlfcl  15690  curf1cl  15696  curfcl  15700  hofcl  15727  yonedainv  15749  pospo  15802  lubfun  15809  glbfun  15822  joindmss  15836  meetdmss  15850  ipopos  15989  acsficl2d  16005  dirref  16064  mgmidcl  16091  mgmlrid  16092  cntzssv  16565  symggrp  16624  symgid  16625  idresperm  16633  pmtrfmvdn0  16686  symggen  16694  psgnunilem1  16717  psgnprfval  16745  slwpgp  16832  frgpmhm  16982  frgpuptinv  16988  frgpup3lem  16994  gsumzoppg  17165  gsumcom2  17199  abv0  17675  rrgsupp  18134  psrvscafval  18238  psrridm  18253  psrridmOLD  18254  ltbwe  18332  psrbag0  18354  psrbagsn  18355  subrgascl  18358  zrhrhm  18724  psgnodpmr  18799  frlmphl  18983  ellspd  19004  mattpostpos  19123  mavmul0  19221  mavmul0g  19222  mdet0f1o  19262  m1detdiag  19266  m2detleiblem5  19294  m2detleiblem6  19295  m2detleiblem3  19298  m2detleiblem4  19299  maducoeval2  19309  d1mat2pmat  19407  chpmat1dlem  19503  chpmat1d  19504  baspartn  19622  eltg3  19630  fctop  19672  cctop  19674  discld  19757  mretopd  19760  neipeltop  19797  neitr  19848  restcls  19849  ordtbaslem  19856  ordtuni  19858  idcn  19925  cnrmi  20028  cmpsublem  20066  cmpsub  20067  tgcmp  20068  uncmp  20070  hauscmplem  20073  cmpfi  20075  bwth  20077  1stcrestlem  20119  disllycmp  20165  dis1stc  20166  refref  20180  kgeni  20204  1stckgenlem  20220  kqffn  20392  snfil  20531  filcon  20550  cfinfil  20560  ufileu  20586  filufint  20587  fixufil  20589  cfinufil  20595  ufilen  20597  fin1aufil  20599  fmf  20612  rnelfm  20620  flimclslem  20651  hauspwpwf1  20654  supnfcls  20687  flimfnfcls  20695  fclscmp  20697  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALT  20717  ptcmplem1  20718  cnextrel  20729  tsmsfbas  20792  ustref  20887  trust  20898  restutop  20906  isusp  20930  xmet0  21011  imasdsf1olem  21042  blfvalps  21052  blfps  21075  blf  21076  restmetu  21256  dscmet  21259  isngp2  21283  nm0  21312  nrginvrcn  21366  nmoix  21402  qdensere  21443  iccconn  21501  iccpnfcnv  21610  xrhmeo  21612  lebnumlem3  21629  cmetss  21919  bcthlem5  21933  rrxmfval  21999  minveclem3b  22009  cniccbdd  22039  ovolicc2lem4  22097  iunmbl  22129  ioorinv  22151  ioorcl  22152  i1f1lem  22262  limcvallem  22441  ellimc2  22447  limccnp  22461  limccnp2  22462  limcco  22463  perfdvf  22473  recnprss  22474  fncpn  22502  dvcmulf  22514  c1lip1  22564  lhop2  22582  q1pcl  22722  r1pdeglt  22725  ply1remlem  22729  plyssc  22763  ulm0  22952  cxpeq0  23227  cxplea  23245  cxplogb  23325  asinlem  23396  isppw2  23587  muval2  23606  dchrfi  23728  dchrpt  23740  bposlem6  23762  lgsdir2lem2  23797  lgsqr  23819  2sqlem7  23843  2sqlem11  23848  chtppilim  23858  tgldimor  24094  tglnfn  24135  tglnunirn  24136  mircinv  24249  perpln1  24288  perpln2  24289  lmiisolem  24362  xmstrkgc  24391  axcgrtr  24420  axsegconlem9  24430  axlowdimlem5  24451  axlowdimlem17  24463  axlowdim1  24464  uhgra0  24511  uhgra0v  24512  umgra0  24527  usgra0  24572  usgra0v  24573  usgraedg4  24589  usgra1v  24592  nb3graprlem1  24653  cusgra1v  24663  cusgraexilem2  24669  uvtx01vtx  24694  wlkcomp  24727  wlkntrl  24766  0spth  24775  1pthonlem1  24793  2pthlem1  24799  usgra2wlkspthlem1  24821  3v3e3cycl1  24846  constr3trllem1  24852  constr3pthlem3  24859  4cycl4v4e  24868  4cycl4dv  24869  0conngra  24876  wwlkn0s  24907  clwlkcomp  24965  frgra0v  25195  frgra1v  25200  1vwmgra  25205  vdgfrgragt2  25229  frgrancvvdeqlem3  25234  frgrawopreg1  25252  frgrawopreg2  25253  2spot0  25266  ex-opab  25355  grpoinvf  25440  ismgmOLD  25520  rngomndo  25621  nvmid  25758  nmlnoubi  25909  hiidrcl  26210  hsn0elch  26364  shjshseli  26609  cmbr4i  26717  dfiop2  26870  kbpj  27073  nmopun  27131  adjeq0  27208  kbass2  27234  pjssdif1i  27292  pjinvari  27308  pjcmul2i  27319  pj3i  27325  stge1i  27355  stle0i  27356  sumdmdlem2  27536  dmdbr6ati  27540  dmdbr7ati  27541  rabsnel  27601  disjdifprg  27646  ofoprabco  27732  padct  27776  fpwrelmapffslem  27786  xrlelttric  27803  iundisj2cnt  27838  nn0min  27845  xrge0tsmsbi  28011  locfinref  28079  dispcmp  28097  pstmxmet  28111  xrge0iifcnv  28150  xrge0iif1  28155  qqhre  28232  esumcl  28259  esumpr2  28296  esumpinfval  28302  esumpcvgval  28307  ofcfn  28329  pwsiga  28360  prsiga  28361  sigainb  28366  measiuns  28425  relfae  28456  sitgf  28553  eulerpartgbij  28575  sgnmulsgn  28752  sgnmulsgp  28753  signswch  28782  signslema  28783  signstlen  28788  subfacp1lem5  28892  erdszelem8  28906  kur14lem1  28914  indispcon  28943  cvmsss2  28983  msubrn  29153  dfpo2  29425  dfon2lem7  29461  wfrlem4  29586  wfrlem14  29596  frrlem6  29636  nosgnn0i  29659  nobndlem2  29693  nobndlem4  29695  nobndlem5  29696  nobndlem6  29697  brbigcup  29776  elsingles  29796  fnimage  29807  funpartlem  29820  dfrdg4  29828  imagesset  29831  altopthsn  29839  elaltxp  29853  ellines  30030  linethru  30031  rankeq1o  30056  elhf2  30060  hfninf  30071  limsucncmpi  30138  volsupnfl  30299  cnambfre  30303  dvasin  30343  dvacos  30344  nn0prpwlem  30380  fneref  30408  neibastop2lem  30418  sdclem2  30475  sstotbnd2  30510  ssbnd  30524  grpokerinj  30587  isdrngo1  30599  ac6s6  30820  prtlem12  30848  elrfirn  30867  ismrcd1  30870  istopclsd  30872  rabren3dioph  30988  jm2.17b  31138  jm2.22  31176  jm2.23  31177  ttac  31217  pw2f1ocnv  31218  dnnumch1  31229  hbtlem5  31318  mncn0  31329  aaitgo  31352  rngunsnply  31363  ssrecnpr  31429  seff  31430  sblpnf  31431  lcmdvds  31455  nzss  31463  dvconstbi  31480  ipo0  31599  ifr0  31600  addrfn  31622  subrfn  31623  mulvfn  31624  refsum2cnlem1  31652  ellimciota  31859  dvmptconst  31949  dvmptidg  31951  dvmulcncf  31961  dvdivcncf  31963  stoweidlem26  32047  stoweidlem50  32071  stoweidlem57  32078  zofldiv2ALTV  32573  2ffzoeq  32715  uhguhgra  32744  uhg0e  32748  uhgres  32751  fusgraimpcl  32799  fusgraimpclALT  32801  0mgm  32834  nnsgrpmgm  32876  c0snmhm  32975  rngchomffvalALTV  33057  funcringcsetcALTV2lem4  33101  funcringcsetclem4ALTV  33124  srhmsubc  33138  rhmsubclem1  33148  srhmsubcALTV  33157  rhmsubcALTVlem1  33167  mapsnop  33188  zlmodzxzldeplem4  33358  nn0o  33393  zofldiv2  33402  fdivval  33414  nnlog2ge0lt1  33441  dig1  33483  bnj145OLD  34183  bnj216  34188  bnj151  34336  bnj517  34344  bnj970  34406  bnj1145  34450  bnj1498  34518  bj-dedthm  34562  bj-speiv  34686  bj-exlimmpbir  34880  bj-snglex  34932  bj-inftyexpidisj  35013  riotasv2d  35085  lkrscss  35220  islshpkrN  35242  isline  35860  ispointN  35863  0psubN  35870  linepsubN  35873  atpsubN  35874  cdlemk36  37036  diafn  37158  dibfna  37278  dibvalrel  37287  dicvalrelN  37309  diclspsn  37318  dihvalrel  37403  dih1  37410  lclkrlem1  37630  lclkr  37657  mapd1o  37772  mapdin  37786  hdmapfnN  37956  hgmapfnN  38015  relexp01min  38219
  Copyright terms: Public domain W3C validator