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  1981  nfald2  2046  nfabd2  2650  dedhb  3273  sbceqal  3387  sbcel12  3823  ssdifeq0  3909  r19.2zb  3918  dedth  3991  pwidg  4023  elpr2  4046  snidg  4053  exsnrex  4065  ifpr  4075  rabrsn  4097  prid1g  4133  pwpw0  4175  sssn  4185  preqr1  4200  pwsnALT  4240  unimax  4281  intmin3  4310  syl6eqbr  4484  intabs  4608  pwnss  4612  0inp0  4619  copsexg  4732  copsexgOLD  4733  euotd  4748  elopab  4755  epelg  4792  ord0eln0  4932  sucidg  4956  nsuceq0  4958  onun2i  4993  elvvuni  5059  posn  5067  frsn  5069  eqrelriv  5094  relopabi  5126  opabid2  5130  ididg  5154  iss  5319  funopg  5618  fn0  5698  f00  5765  f0bi  5766  f1o00  5846  fo00  5847  brprcneu  5857  dffn5  5911  fsn  6057  fnsnb  6078  fconstfv  6121  eufnfv  6132  f1eqcocnv  6190  nfriotad  6251  riotaprop  6267  oprabid  6306  elrnmpt2  6397  ov6g  6422  ovelrn  6433  caovmo  6494  offn  6533  caofinvl  6549  fr3nr  6593  onprc  6598  ordeleqon  6602  onint0  6609  0elsuc  6648  onuninsuci  6653  orduninsuc  6656  ordzsl  6658  onzsl  6659  tfinds  6672  limomss  6683  limom  6693  peano5  6701  xpexr  6721  eqop2  6822  1stconst  6868  2ndconst  6869  funsssuppss  6923  dftpos3  6970  dftpos4  6971  oawordeulem  7200  omwordi  7217  nnmwordi  7281  riiner  7381  ecopover  7412  map0g  7455  mapsn  7457  elixpsn  7505  en0  7575  en1  7579  fiprc  7594  sbthlem2  7625  sbthlem4  7627  sbthlem5  7628  nneneq  7697  sdom1  7716  fineqvlem  7731  nfielex  7745  findcard  7755  findcard2  7756  elfiun  7886  marypha1lem  7889  oicl  7950  oif  7951  oion  7957  hartogslem1  7963  hartogs  7965  wemapso2  7975  card2on  7976  0wdom  7992  brwdom2  7995  sucprcregOLD  8022  inf3lem6  8046  noinfepOLD  8073  cantnflem3  8106  cantnflem4  8107  cantnflem3OLD  8128  cantnflem4OLD  8129  wemapwe  8135  wemapweOLD  8136  cnfcom  8140  cnfcomOLD  8148  tctr  8167  r1tr  8190  r1rankidb  8218  r1pw  8259  scottex  8299  scott0  8300  bnd2  8307  tskwe  8327  oncard  8337  cardlim  8349  harsdom  8372  en2eleq  8382  dfac8alem  8406  cardaleph  8466  iunfictbso  8491  infmap2  8594  ackbij1lem18  8613  cff  8624  cfsuc  8633  cff1  8634  cflim2  8639  cfss  8641  sdom2en01  8678  infpssrlem4  8682  fin23lem7  8692  fin23lem11  8693  isfin2-2  8695  fin23lem26  8701  fin23lem19  8712  fin23lem17  8714  isf34lem2  8749  isf34lem4  8753  fin1a2lem6  8781  fin1a2lem10  8785  fin1a2lem12  8787  itunifn  8793  hsmexlem1  8802  axcc2lem  8812  dcomex  8823  axdc3lem4  8829  ondomon  8934  konigthlem  8939  pwcfsdom  8954  cfpwsdom  8955  axpowndlem3  8971  axpowndlem3OLD  8972  canth4  9021  canthnumlem  9022  canthwelem  9024  canthwe  9025  canthp1lem2  9027  pwfseqlem4  9036  pwfseqlem5  9037  gchaleph  9045  gch2  9049  winainflem  9067  0tsk  9129  rankcf  9151  tskcard  9155  gruina  9192  grutsk  9196  tskmid  9214  indpi  9281  nqereu  9303  mulcanenq  9334  recmulnq  9338  archnq  9354  ltsopr  9406  1ne0sr  9469  0idsr  9470  00sr  9472  leid  9676  lelttric  9687  divcan3  10227  lemul1a  10392  nn1suc  10553  nn0n0n1ge2b  10856  nn0ind-raph  10957  elnn1uz2  11154  indstr2  11156  uzsupss  11170  rpnnen1lem4  11207  rpnnen1lem5  11208  xrnemnf  11324  xrnepnf  11325  mnfltxr  11332  nn0pnfge0  11337  xrlttri  11341  xrlttr  11342  xrleid  11352  qbtwnxr  11395  xmullem2  11453  xlemul1a  11476  xrub  11499  ixxun  11541  fztpval  11737  fseq1p1m1  11748  elfznelfzob  11880  ltweuz  12036  fzfi  12046  fsuppmapnn0fiubex  12062  ser0f  12124  0exp  12165  faclbnd4lem1  12335  bcn1  12355  hashnemnf  12381  hashv01gt1  12382  hashle00  12427  hashgt12el2  12443  hashmap  12455  hashpw  12456  hashf1  12468  fz1isolem  12472  hash2prd  12480  hash2prv  12487  0wrd0  12528  wrdlen1  12540  ccatvalfn  12560  swrdlen  12609  swrdvalfn  12622  swrdspsleq  12632  cats1un  12660  wrdind  12661  wrd2ind  12662  swrdccatin1  12667  repswsymballbi  12711  cshw1  12749  sqr0lem  13033  sqrtsq  13062  mptfzshft  13552  fsumrev  13553  egt2lt3  13796  0dvds  13861  bitsp1o  13938  gcddvds  14008  bezout  14035  1nprm  14077  prmind2  14083  rpdvds  14120  pcpre1  14221  vdwapf  14345  vdwapid1  14348  ram0  14395  ramz  14398  cshws0  14440  prmlem0  14445  strle1  14582  restsspw  14683  prdsdsfn  14716  imasdsfn  14765  imasaddfnlem  14779  imasvscafn  14788  xpscfv  14813  xpsfrnel  14814  isacs1i  14908  cidfn  14930  comffn  14957  isoval  15016  sscres  15049  cofucl  15111  idffth  15156  ressffth  15161  catcoppccl  15289  1stfcl  15320  2ndfcl  15321  prfcl  15326  evlfcl  15345  curf1cl  15351  curfcl  15355  hofcl  15382  yonedainv  15404  pospo  15456  lubfun  15463  glbfun  15476  joindmss  15490  meetdmss  15504  ipopos  15643  acsficl2d  15659  dirref  15718  mgmidcl  15749  mgmlrid  15750  cntzssv  16161  symggrp  16220  symgid  16221  idresperm  16229  pmtrfmvdn0  16283  symggen  16291  psgnunilem1  16314  psgnprfval  16342  slwpgp  16429  frgpmhm  16579  frgpuptinv  16585  frgpup3lem  16591  gsumcom2  16794  abv0  17263  rrgsupp  17710  psrvscafval  17814  psrridm  17829  psrridmOLD  17830  ltbwe  17908  psrbag0  17930  psrbagsn  17931  subrgascl  17934  zrhrhm  18316  psgnodpmr  18393  frlmphl  18579  ellspd  18603  ellspdOLD  18604  mattpostpos  18723  mavmul0  18821  mavmul0g  18822  mdet0f1o  18862  m1detdiag  18866  m2detleiblem5  18894  m2detleiblem6  18895  m2detleiblem3  18898  m2detleiblem4  18899  maducoeval2  18909  d1mat2pmat  19007  chpmat1dlem  19103  chpmat1d  19104  baspartn  19222  eltg3  19230  fctop  19271  cctop  19273  discld  19356  mretopd  19359  neipeltop  19396  neitr  19447  restcls  19448  ordtbaslem  19455  ordtuni  19457  idcn  19524  cnrmi  19627  cmpsublem  19665  cmpsub  19666  tgcmp  19667  uncmp  19669  hauscmplem  19672  cmpfi  19674  bwth  19676  bwthOLD  19677  1stcrestlem  19719  disllycmp  19765  dis1stc  19766  kgeni  19773  1stckgenlem  19789  kqffn  19961  snfil  20100  filcon  20119  cfinfil  20129  ufileu  20155  filufint  20156  fixufil  20158  cfinufil  20164  ufilen  20166  fin1aufil  20168  fmf  20181  rnelfm  20189  flimclslem  20220  hauspwpwf1  20223  supnfcls  20256  flimfnfcls  20264  fclscmp  20266  alexsubALTlem2  20283  alexsubALTlem3  20284  alexsubALT  20286  ptcmplem1  20287  cnextrel  20298  tsmsfbas  20361  ustref  20456  trust  20467  restutop  20475  isusp  20499  xmet0  20580  imasdsf1olem  20611  blfvalps  20621  blfps  20644  blf  20645  restmetu  20825  dscmet  20828  isngp2  20852  nm0  20881  nrginvrcn  20935  nmoix  20971  qdensere  21012  iccconn  21070  iccpnfcnv  21179  xrhmeo  21181  lebnumlem3  21198  cmetss  21488  bcthlem5  21502  rrxmfval  21568  minveclem3b  21578  cniccbdd  21608  ovolicc2lem4  21666  iunmbl  21698  ioorinv  21720  ioorcl  21721  i1f1lem  21831  limcvallem  22010  ellimc2  22016  limccnp  22030  limccnp2  22031  limcco  22032  perfdvf  22042  recnprss  22043  fncpn  22071  dvcmulf  22083  c1lip1  22133  lhop2  22151  q1pcl  22291  r1pdeglt  22294  ply1remlem  22298  plyssc  22332  ulm0  22520  cxpeq0  22787  cxplea  22805  asinlem  22927  isppw2  23117  muval2  23136  dchrfi  23258  dchrpt  23270  bposlem6  23292  lgsdir2lem2  23327  lgsqr  23349  2sqlem7  23373  2sqlem11  23378  chtppilim  23388  tgldimor  23621  tglnfn  23662  tglnunirn  23663  mircinv  23761  perpln1  23795  perpln2  23796  lmiisolem  23838  xmstrkgc  23865  axcgrtr  23894  axsegconlem9  23904  axlowdimlem5  23925  axlowdimlem17  23937  axlowdim1  23938  uhgra0  23985  uhgra0v  23986  umgra0  24001  usgra0  24046  usgra0v  24047  usgraedg4  24063  usgra1v  24066  nb3graprlem1  24127  cusgra1v  24137  cusgraexilem2  24143  uvtx01vtx  24168  wlkcomp  24201  wlkntrl  24240  0spth  24249  1pthonlem1  24267  2pthlem1  24273  3v3e3cycl1  24320  constr3trllem1  24326  constr3pthlem3  24333  4cycl4v4e  24342  4cycl4dv  24343  0conngra  24350  wwlkn0s  24381  clwlkcomp  24439  frgra0v  24669  frgra1v  24674  1vwmgra  24679  vdgfrgragt2  24704  frgrancvvdeqlem3  24709  frgrawopreg1  24727  frgrawopreg2  24728  2spot0  24741  ex-opab  24830  grpoinvf  24918  ismgm  24998  rngomndo  25099  nvmid  25236  nmlnoubi  25387  hiidrcl  25688  hsn0elch  25842  shjshseli  26087  cmbr4i  26195  dfiop2  26348  kbpj  26551  nmopun  26609  adjeq0  26686  kbass2  26712  pjssdif1i  26770  pjinvari  26786  pjcmul2i  26797  pj3i  26803  stge1i  26833  stle0i  26834  sumdmdlem2  27014  dmdbr6ati  27018  dmdbr7ati  27019  rabsnel  27078  disjdifprg  27109  ofoprabco  27177  fpwrelmapffslem  27227  xrlelttric  27240  iundisj2cnt  27272  nn0min  27279  xrge0tsmsbi  27439  pstmxmet  27512  xrge0iifcnv  27551  xrge0iif1  27556  qqhre  27634  esumcl  27683  esumpr2  27714  esumpinfval  27719  esumpcvgval  27724  ofcfn  27739  pwsiga  27770  prsiga  27771  sigainb  27776  measiuns  27828  relfae  27859  sitgf  27929  eulerpartgbij  27951  sgnmulsgn  28128  sgnmulsgp  28129  plymulx  28145  signswch  28158  signslema  28159  signstlen  28164  subfacp1lem5  28268  erdszelem8  28282  kur14lem1  28290  indispcon  28319  cvmsss2  28359  relexpsucr  28528  prodf1f  28603  fprodshft  28683  fprodrev  28684  dfpo2  28761  dfon2lem7  28798  wfrlem4  28923  wfrlem14  28933  frrlem6  28973  nosgnn0i  28996  nobndlem2  29030  nobndlem4  29032  nobndlem5  29033  nobndlem6  29034  brbigcup  29125  elsingles  29145  fnimage  29156  funpartlem  29169  dfrdg4  29177  imagesset  29180  altopthsn  29188  elaltxp  29202  ellines  29379  linethru  29380  rankeq1o  29405  elhf2  29409  hfninf  29420  limsucncmpi  29487  volsupnfl  29636  cnambfre  29640  dvasin  29680  dvacos  29681  nn0prpwlem  29717  fneref  29756  refref  29757  neibastop2lem  29781  sdclem2  29838  sstotbnd2  29873  ssbnd  29887  grpokerinj  29950  isdrngo1  29962  ac6s6  30184  prtlem12  30212  elrfirn  30231  ismrcd1  30234  istopclsd  30236  rabren3dioph  30353  jm2.17b  30503  jm2.22  30541  jm2.23  30542  ttac  30582  pw2f1ocnv  30583  dnnumch1  30594  hbtlem5  30681  mncn0  30693  aaitgo  30716  rngunsnply  30727  ssrecnpr  30791  seff  30792  sblpnf  30793  lcmdvds  30814  nzss  30822  dvconstbi  30839  ipo0  30936  ifr0  30937  addrfn  30959  subrfn  30960  mulvfn  30961  refsum2cnlem1  30990  stoweidlem26  31326  stoweidlem50  31350  stoweidlem57  31357  2ffzoeq  31810  uhguhgra  31841  uhg0e  31845  uhgres  31848  fusgraimpcl  31896  fusgraimpclALT  31898  zlmodzxzldeplem4  32185  bnj145OLD  32862  bnj216  32867  bnj151  33014  bnj517  33022  bnj970  33084  bnj1014  33097  bnj1145  33128  bnj1498  33196  bj-dedthm  33241  bj-speiv  33367  bj-exlimmpbir  33560  bj-snglex  33612  bj-inftyexpidisj  33685  riotasv2d  33760  lkrscss  33895  islshpkrN  33917  isline  34535  ispointN  34538  0psubN  34545  linepsubN  34548  atpsubN  34549  cdlemk36  35709  diafn  35831  dibfna  35951  dibvalrel  35960  dicvalrelN  35982  diclspsn  35991  dihvalrel  36076  dih1  36083  lclkrlem1  36303  lclkr  36330  mapd1o  36445  mapdin  36459  hdmapfnN  36629  hgmapfnN  36688
  Copyright terms: Public domain W3C validator