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

Theorem mpbiri 236
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 235 1  |-  ( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  dedt  965  spei  2071  nfald2  2133  nfabd2  2582  raleleqALT  2977  dedhb  3176  sbceqal  3287  ssdifeq0  3816  r19.2zb  3825  dedth  3898  pwidg  3930  elpr2  3953  snidg  3960  exsnrex  3973  ifpr  3984  rabrsn  4006  prid1g  4042  pwpw0  4084  sssn  4094  preqr1  4110  pwsnALT  4150  unimax  4190  intmin3  4220  syl6eqbr  4397  intabs  4521  pwnss  4525  0inp0  4532  copsexg  4642  euotd  4657  elopab  4664  epelg  4701  elvvuni  4850  posn  4858  frsn  4860  eqrelriv  4883  relopabi  4914  opabid2  4919  ididg  4943  iss  5107  ord0eln0  5432  sucidg  5456  nsuceq0  5458  onun2i  5493  funopg  5569  fn0  5649  f00  5718  f0bi  5719  f10d  5799  f1o00  5800  fo00  5801  brprcneu  5811  dffn5  5863  fsn  6013  fnsnb  6035  fconstfvOLD  6079  eufnfv  6091  f1eqcocnv  6151  nfriotad  6212  riotaprop  6227  oprabid  6269  elrnmpt2  6360  ov6g  6385  ovelrn  6396  caovmo  6457  offn  6493  caofinvl  6509  fr3nr  6557  onprc  6562  ordeleqon  6566  onint0  6574  0elsuc  6613  onuninsuci  6618  orduninsuc  6621  ordzsl  6623  onzsl  6624  tfinds  6637  limomss  6648  limom  6658  peano5  6667  xpexr  6684  eqop2  6785  1stconst  6832  2ndconst  6833  funsssuppss  6889  dftpos3  6939  dftpos4  6940  wfrlem4  6987  wfrlem14  6997  oawordeulem  7203  omwordi  7220  nnmwordi  7284  riiner  7384  ecopover  7415  map0g  7459  mapsn  7461  elixpsn  7509  en0  7579  en1  7583  fiprc  7598  sbthlem2  7629  sbthlem4  7631  sbthlem5  7632  nneneq  7701  sdom1  7718  fineqvlem  7732  nfielex  7746  findcard  7756  findcard2  7757  elfiun  7890  marypha1lem  7893  oicl  7990  oif  7991  oion  7997  hartogslem1  8003  hartogs  8005  wemapso2  8014  card2on  8015  0wdom  8031  brwdom2  8034  inf3lem6  8084  cantnflem3  8141  cantnflem4  8142  wemapwe  8147  cnfcom  8150  tctr  8169  r1tr  8192  r1rankidb  8220  r1pw  8261  scottex  8301  scott0  8302  bnd2  8309  tskwe  8329  oncard  8339  cardlim  8351  harsdom  8374  en2eleq  8384  dfac8alem  8404  cardaleph  8464  iunfictbso  8489  infmap2  8592  ackbij1lem18  8611  cff  8622  cfsuc  8631  cff1  8632  cflim2  8637  cfss  8639  sdom2en01  8676  infpssrlem4  8680  fin23lem7  8690  fin23lem11  8691  isfin2-2  8693  fin23lem26  8699  fin23lem19  8710  fin23lem17  8712  isf34lem2  8747  isf34lem4  8751  fin1a2lem6  8779  fin1a2lem10  8783  fin1a2lem12  8785  itunifn  8791  hsmexlem1  8800  axcc2lem  8810  dcomex  8821  axdc3lem4  8827  ondomon  8932  konigthlem  8937  pwcfsdom  8952  cfpwsdom  8953  axpowndlem3  8968  canth4  9016  canthnumlem  9017  canthwelem  9019  canthwe  9020  canthp1lem2  9022  pwfseqlem4  9031  pwfseqlem5  9032  gchaleph  9040  gch2  9044  winainflem  9062  0tsk  9124  rankcf  9146  tskcard  9150  gruina  9187  grutsk  9191  tskmid  9209  indpi  9276  nqereu  9298  mulcanenq  9329  recmulnq  9333  archnq  9349  ltsopr  9401  1ne0sr  9464  0idsr  9465  00sr  9467  leid  9673  lelttric  9685  divcan3  10238  lemul1a  10403  nn1suc  10574  nn0n0n1ge2b  10877  nn0lt10b  10942  nn0ind-raph  10979  elnn1uz2  11179  indstr2  11181  uzsupss  11200  rpnnen1lem4  11237  rpnnen1lem5  11238  xrnemnf  11363  xrnepnf  11364  mnfltxr  11373  nn0pnfge0  11378  xrlttri  11382  xrlttr  11383  xrleid  11393  qbtwnxr  11437  xmullem2  11495  xlemul1a  11518  xrub  11541  reltxrnmnf  11576  ixxun  11595  fztpval  11801  fseq1p1m1  11812  elfznelfzob  11958  ltweuz  12118  fzfi  12128  fsuppmapnn0fiubex  12147  ser0f  12209  0exp  12250  faclbnd4lem1  12421  bcn1  12441  hashnemnf  12470  hashv01gt1  12471  hashle00  12520  hashgt12el2  12537  hashmap  12548  hashpw  12549  hashf1  12561  fz1isolem  12565  hash2prb  12574  0wrd0  12634  wrdlen1  12646  ccatvalfn  12667  swrdlen  12718  swrdspsleq  12744  cats1un  12771  wrdind  12772  wrd2ind  12773  swrdccatin1  12778  repswsymballbi  12822  cshw1  12860  scshwfzeqfzo  12864  trclfvcotr  13010  relexp1g  13026  relexp0rel  13037  relexprelg  13038  sqr0lem  13241  sqrtsq  13270  mptfzshft  13775  fsumrev  13776  prodf1f  13884  fprodrev  13967  egt2lt3  14194  0dvds  14259  bitsp1o  14342  gcddvds  14413  bezout  14446  lcmdvds  14509  1nprm  14565  prmind2  14571  rpdvds  14612  pcpre1  14728  vdwapf  14858  vdwapid1  14861  ram0  14916  ramz  14919  prmolefac  14940  cshws0  15008  prmlem0  15013  strle1  15157  restsspw  15266  prdsdsfn  15299  imasdsfn  15351  imasdsfnOLD  15363  imasaddfnlem  15370  imasvscafn  15379  xpscfv  15404  xpsfrnel  15405  isacs1i  15499  cidfn  15521  fnhomeqhomf  15532  comffn  15546  isoval  15606  sscres  15664  cofucl  15729  idffth  15774  ressffth  15779  catcoppccl  15939  estrchomfn  15956  funcestrcsetclem4  15964  funcestrcsetclem7  15967  equivestrcsetc  15973  funcsetcestrclem4  15979  funcsetcestrclem7  15982  1stfcl  16018  2ndfcl  16019  prfcl  16024  evlfcl  16043  curf1cl  16049  curfcl  16053  hofcl  16080  yonedainv  16102  pospo  16155  lubfun  16162  glbfun  16175  joindmss  16189  meetdmss  16203  ipopos  16342  acsficl2d  16358  dirref  16417  mgmidcl  16444  mgmlrid  16445  cntzssv  16918  symggrp  16977  symgid  16978  idresperm  16986  pmtrfmvdn0  17039  symggen  17047  psgnunilem1  17070  psgnprfval  17098  slwpgp  17201  frgpmhm  17351  frgpuptinv  17357  frgpup3lem  17363  gsumzoppg  17513  gsumcom2  17543  abv0  17995  rrgsupp  18451  psrvscafval  18550  psrridm  18564  ltbwe  18632  psrbag0  18653  psrbagsn  18654  subrgascl  18657  zrhrhm  19018  psgnodpmr  19093  frlmphl  19274  ellspd  19295  mattpostpos  19414  mavmul0  19512  mavmul0g  19513  mdet0f1o  19553  m1detdiag  19557  m2detleiblem5  19585  m2detleiblem6  19586  m2detleiblem3  19589  m2detleiblem4  19590  maducoeval2  19600  d1mat2pmat  19698  chpmat1dlem  19794  chpmat1d  19795  baspartn  19904  eltg3  19912  fctop  19954  cctop  19956  discld  20040  mretopd  20043  neipeltop  20080  neitr  20131  restcls  20132  ordtbaslem  20139  ordtuni  20141  idcn  20208  cnrmi  20311  cmpsublem  20349  cmpsub  20350  tgcmp  20351  uncmp  20353  hauscmplem  20356  cmpfi  20358  bwth  20360  1stcrestlem  20402  disllycmp  20448  dis1stc  20449  refref  20463  kgeni  20487  1stckgenlem  20503  kqffn  20675  snfil  20814  filcon  20833  cfinfil  20843  ufileu  20869  filufint  20870  fixufil  20872  cfinufil  20878  ufilen  20880  fin1aufil  20882  fmf  20895  rnelfm  20903  flimclslem  20934  hauspwpwf1  20937  supnfcls  20970  flimfnfcls  20978  fclscmp  20980  alexsubALTlem2  20998  alexsubALTlem3  20999  alexsubALT  21001  ptcmplem1  21002  cnextrel  21013  tsmsfbas  21077  ustref  21168  trust  21179  restutop  21187  isusp  21211  xmet0  21292  imasdsf1olem  21323  blfvalps  21333  blfps  21356  blf  21357  restmetu  21520  dscmet  21522  isngp2  21546  nm0  21575  nrginvrcn  21629  nmoix  21669  nmoixOLD  21685  qdensere  21725  iccconn  21783  iccpnfcnv  21907  xrhmeo  21909  lebnumlem3  21926  lebnumlem3OLD  21929  cmetss  22219  bcthlem5  22231  rrxmfval  22295  minveclem3b  22305  minveclem3bOLD  22317  cniccbdd  22347  ovolicc2lem4OLD  22408  ovolicc2lem4  22409  iunmbl  22441  ioorinv  22463  ioorcl  22464  ioorinvOLD  22468  ioorclOLD  22469  i1f1lem  22582  limcvallem  22761  ellimc2  22767  limccnp  22781  limccnp2  22782  limcco  22783  perfdvf  22793  recnprss  22794  fncpn  22822  dvcmulf  22834  c1lip1  22884  lhop2  22902  q1pcl  23041  r1pdeglt  23044  ply1remlem  23048  plyssc  23089  ulm0  23281  cxpeq0  23558  cxplea  23576  cxplogb  23658  asinlem  23729  isppw2  23977  muval2  23996  dchrfi  24118  dchrpt  24130  bposlem6  24152  lgsdir2lem2  24187  lgsqr  24209  2sqlem7  24233  2sqlem11  24238  chtppilim  24248  tgldimor  24481  tgcgr4  24511  tglnfn  24527  tglnunirn  24528  mirne  24647  mircinv  24648  perpln1  24690  perpln2  24691  lmiisolem  24773  xmstrkgc  24851  axcgrtr  24880  axsegconlem9  24890  axlowdimlem5  24911  axlowdimlem17  24923  axlowdim1  24924  uhgra0  24971  uhgra0v  24972  umgra0  24987  usgra0v  25033  usgraedg4  25049  usgra1v  25052  usgraexmpl  25064  nb3graprlem1  25114  cusgra1v  25124  cusgraexilem2  25130  uvtx01vtx  25155  wlkcomp  25188  wlkntrl  25227  0spth  25236  1pthonlem1  25254  2pthlem1  25260  usgra2wlkspthlem1  25282  3v3e3cycl1  25307  constr3trllem1  25313  constr3pthlem3  25320  4cycl4v4e  25329  4cycl4dv  25330  0conngra  25337  wwlkn0s  25368  clwlkcomp  25426  frgra0v  25656  frgra1v  25661  1vwmgra  25666  vdgfrgragt2  25690  frgrancvvdeqlem3  25695  frgrawopreg1  25713  frgrawopreg2  25714  2spot0  25727  ex-opab  25817  grpoinvf  25903  ismgmOLD  25983  rngomndo  26084  nvmid  26221  nmlnoubi  26372  hiidrcl  26683  hsn0elch  26836  shjshseli  27081  cmbr4i  27189  dfiop2  27341  kbpj  27544  nmopun  27602  adjeq0  27679  kbass2  27705  pjssdif1i  27763  pjinvari  27779  pjcmul2i  27790  pj3i  27796  stge1i  27826  stle0i  27827  sumdmdlem2  28007  dmdbr6ati  28011  dmdbr7ati  28012  rabsnel  28074  disjdifprg  28124  ofoprabco  28206  padct  28250  fpwrelmapffslem  28260  xrlelttric  28272  iundisj2cnt  28318  f1ocnt  28319  fz1nnct  28320  fz1nntr  28321  nn0min  28328  xrge0tsmsbi  28494  locfinref  28613  dispcmp  28631  pstmxmet  28645  xrge0iifcnv  28684  xrge0iif1  28689  qqhre  28769  esumcl  28796  esumpr2  28833  esumpinfval  28839  esumpcvgval  28844  ofcfn  28866  pwsiga  28897  prsiga  28898  sigainb  28903  ldgenpisyslem1  28930  measiuns  28984  relfae  29015  pmeasmono  29102  sitgf  29125  eulerpartgbij  29150  sgnmulsgn  29365  sgnmulsgp  29366  signswch  29395  signslema  29396  signstlen  29401  bnj145OLD  29480  bnj216  29485  bnj151  29633  bnj517  29641  bnj970  29703  bnj1145  29747  bnj1498  29815  subfacp1lem5  29852  erdszelem8  29866  kur14lem1  29874  indispcon  29902  cvmsss2  29942  msubrn  30112  dfpo2  30339  dfon2lem7  30379  frrlem6  30467  nosgnn0i  30490  nobndlem2  30524  nobndlem4  30526  nobndlem5  30527  nobndlem6  30528  brbigcup  30607  elsingles  30627  fnimage  30638  funpartlem  30651  dfrdg4  30660  imagesset  30662  altopthsn  30670  elaltxp  30684  ellines  30861  linethru  30862  rankeq1o  30880  elhf2  30884  hfninf  30895  nn0prpwlem  30920  fneref  30948  neibastop2lem  30958  limsucncmpi  31047  bj-dedthm  31096  bj-speiv  31222  bj-exlimmpbir  31420  bj-snglex  31472  bj-inftyexpidisj  31553  topdifinffinlem  31651  relowlssretop  31667  rdgeqoa  31674  finxpreclem6  31689  poimirlem23  31864  poimirlem29  31870  poimirlem31  31872  volsupnfl  31886  cnambfre  31890  dvasin  31929  dvacos  31930  sdclem2  31972  sstotbnd2  32007  ssbnd  32021  grpokerinj  32084  isdrngo1  32096  ac6s6  32316  prtlem12  32344  riotasv2d  32435  lkrscss  32570  islshpkrN  32592  isline  33210  ispointN  33213  0psubN  33220  linepsubN  33223  atpsubN  33224  cdlemk36  34386  diafn  34508  dibfna  34628  dibvalrel  34637  dicvalrelN  34659  diclspsn  34668  dihvalrel  34753  dih1  34760  lclkrlem1  34980  lclkr  35007  mapd1o  35122  mapdin  35136  hdmapfnN  35306  hgmapfnN  35365  elrfirn  35443  ismrcd1  35446  istopclsd  35448  rabren3dioph  35564  jm2.17b  35718  jm2.22  35757  jm2.23  35758  ttac  35798  pw2f1ocnv  35799  dnnumch1  35809  hbtlem5  35894  mncn0  35905  aaitgo  35935  rngunsnply  35946  clcnvlem  36137  relexp01min  36212  ssrecnpr  36563  seff  36564  sblpnf  36565  nzss  36573  dvconstbi  36590  ipo0  36709  ifr0  36710  addrfn  36732  subrfn  36733  mulvfn  36734  refsum2cnlem1  37268  ellimciota  37571  dvmptconst  37662  dvmptidg  37664  dvmulcncf  37674  dvdivcncf  37676  stoweidlem26  37763  stoweidlem50  37788  stoweidlem57  37795  iccpartiltu  38543  iccpartigtl  38544  zofldiv2ALTV  38598  evenprm2  38649  stgoldbwt  38684  nnsum3primesle9  38696  nnsum4primeseven  38702  nnsum4primesevenALTV  38703  tgblthelfgott  38715  funop  38819  funop1  38820  funsndifnop  38822  funsneqopsn  38823  fun2dmnopgexmpl  38828  2ffzoeq  38855  uhgruhgra  38928  uhgr0e  38932  usgr1vr  39063  issubgr2  39075  subgrprop2  39077  egrsubgr  39080  0grsubgr  39081  0uhgrsubgr  39082  uhgrsubgrself  39083  nbgr0vtx  39154  nbgr1vtx  39156  nb3grprlem1  39179  uvtxa0  39190  uvtxa01vtx0  39193  cplgr0v  39217  usgrexi  39228  uhguhgra  39269  uhg0e  39273  uhgres  39276  fusgraimpcl  39324  fusgraimpclALT  39326  0mgm  39359  nnsgrpmgm  39401  c0snmhm  39500  rngchomffvalALTV  39582  funcringcsetcALTV2lem4  39626  funcringcsetclem4ALTV  39649  srhmsubc  39663  rhmsubclem1  39673  srhmsubcALTV  39682  rhmsubcALTVlem1  39692  mapsnop  39713  zlmodzxzldeplem4  39883  nn0o  39916  zofldiv2  39925  fdivval  39937  nnlog2ge0lt1  39964  dig1  40006
  Copyright terms: Public domain W3C validator