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

Theorem mpbiri 224
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 10 . 2  |-  ( ph  ->  ch )
3 mpbiri.maj . 2  |-  ( ph  ->  ( ps  <->  ch )
)
42, 3mpbird 223 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  dedt  923  nfald2  1912  nfabd2  2437  dedhb  2935  sbceqal  3042  ssdifeq0  3536  r19.2zb  3544  dedth  3606  pwidg  3637  elpr2  3659  snidg  3665  ifpr  3681  prid1g  3732  pwpw0  3763  sssn  3772  preqr1  3786  pwsnALT  3822  unimax  3861  intmin3  3890  syl6eqbr  4060  intabs  4172  pwnss  4176  0inp0  4182  copsexg  4252  euotd  4267  elopab  4272  epelg  4306  ord0eln0  4446  sucidg  4470  nsuceq0  4472  onun2i  4508  fr3nr  4571  onprc  4576  ordeleqon  4580  onint0  4587  0elsuc  4626  onuninsuci  4631  orduninsuc  4634  ordzsl  4636  onzsl  4637  tfinds  4650  limomss  4661  limom  4671  peano5  4679  elvvuni  4750  posn  4758  frsn  4760  eqrelriv  4780  relopabi  4811  opabid2  4815  ididg  4837  iss  4998  dmxpss  5107  xpexr  5114  iotassuni  5235  funopg  5286  fn0  5363  f00  5426  f1o00  5508  fo00  5509  brprcneu  5518  dffn5  5568  fsn  5696  fconstfv  5734  eufnfv  5752  f1eqcocnv  5805  oprabid  5882  elrnmpt2  5957  ov6g  5985  ovelrn  5996  caovmo  6057  offn  6089  caofinvl  6104  eqop2  6163  1stconst  6207  2ndconst  6208  dftpos3  6252  dftpos4  6253  nfriotad  6313  riotaprop  6328  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  riotasv3dOLD  6354  oawordeulem  6552  omwordi  6569  omwordri  6570  nnmwordi  6633  riiner  6732  ecopover  6762  map0e  6805  map0g  6807  mapsn  6809  elixpsn  6855  en0  6924  en1  6928  fiprc  6942  sbthlem2  6972  sbthlem4  6974  sbthlem5  6975  fodomr  7012  nneneq  7044  sdom1  7062  fineqvlem  7077  findcard  7097  findcard2  7098  fipwuni  7179  fipwss  7182  elfiun  7183  marypha1lem  7186  ordtypelem6  7238  oicl  7244  oif  7245  oion  7251  hartogslem1  7257  hartogs  7259  card2on  7268  0wdom  7284  brwdom2  7287  sucprcreg  7313  inf3lemd  7328  inf3lem6  7334  noinfepOLD  7361  cantnfle  7372  cantnflem2  7392  cantnflem3  7393  cantnflem4  7394  wemapwe  7400  cnfcom  7403  tctr  7425  r1tr  7448  r1rankidb  7476  r1pw  7517  scottex  7555  scott0  7556  bnd2  7563  tskwe  7583  oncard  7593  cardlim  7605  harsdom  7628  dfac8alem  7656  cardaleph  7716  iunfictbso  7741  infmap2  7844  ackbij1lem18  7863  cff  7874  cfub  7875  cflecard  7879  cfle  7880  cfsuc  7883  cff1  7884  cflim2  7889  cfss  7891  sdom2en01  7928  infpssrlem4  7932  fin23lem7  7942  fin23lem11  7943  isfin2-2  7945  fin23lem26  7951  fin23lem19  7962  fin23lem17  7964  fin23lem29  7967  compsscnvlem  7996  isf34lem2  7999  isf34lem4  8003  fin1a2lem6  8031  fin1a2lem10  8035  fin1a2lem12  8037  itunifn  8043  itunitc1  8046  hsmexlem1  8052  axcc2lem  8062  dcomex  8073  axdc3lem4  8079  ondomon  8185  konigthlem  8190  pwcfsdom  8205  cfpwsdom  8206  axpowndlem3  8221  canth4  8269  canthnumlem  8270  canthwelem  8272  canthwe  8273  canthp1lem2  8275  pwfseqlem4  8284  pwfseqlem5  8285  gchaleph  8297  gch2  8301  winainflem  8315  0tsk  8377  rankcf  8399  tskcard  8403  gruina  8440  grur1a  8441  grutsk  8444  tskmid  8462  indpi  8531  nqereu  8553  mulcanenq  8584  recmulnq  8588  archnq  8604  ltsopr  8656  1ne0sr  8718  0idsr  8719  00sr  8721  leid  8916  lelttric  8927  divcan3  9448  lemul1a  9610  nn1suc  9767  nn0ind-raph  10112  elnn1uz2  10294  indstr2  10296  uzsupss  10310  rpnnen1lem4  10345  rpnnen1lem5  10346  xrnemnf  10460  xrnepnf  10461  mnfltxr  10466  xrlttri  10473  xrlttr  10474  xrleid  10484  qbtwnxr  10527  xmullem2  10585  xlemul1a  10608  xrub  10630  ixxun  10672  fztpval  10845  fseq1p1m1  10857  ltweuz  11024  fzfi  11034  ser0f  11099  0exp  11137  faclbnd4lem1  11306  bcn1  11325  hashmap  11387  hashpw  11388  hashf1  11395  fz1isolem  11399  swrdlen  11456  cats1un  11476  wrdind  11477  sqr0lem  11726  sqrsq  11755  fsumrev  12241  fsumshft  12242  egt2lt3  12484  0dvds  12549  bitsp1o  12624  sadcaddlem  12648  sadcl  12653  smupvallem  12674  smucl  12675  gcddvds  12694  bezout  12721  1nprm  12763  prmind2  12769  rpdvds  12803  pcpre1  12895  vdwapf  13019  vdwapid1  13022  ram0  13069  ramz  13072  prmlem0  13107  strfvss  13166  strle1  13239  restsspw  13336  prdsless  13362  prdsdsfn  13364  imasdsfn  13417  imasaddfnlem  13430  imasvscafn  13439  xpscfv  13464  xpsfrnel  13465  isacs1i  13559  cidfn  13581  comffn  13608  isoval  13667  sscres  13700  cofucl  13762  idffth  13807  ressffth  13812  catcoppccl  13940  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  yonedainv  14055  pospo  14107  ipopos  14263  acsficl2d  14279  dirref  14357  mgmidcl  14388  mgmlrid  14389  symggrp  14780  symgid  14781  cntzssv  14804  slwpgp  14924  frgpmhm  15074  frgpuptinv  15080  frgpup3lem  15086  gsumcom2  15226  abv0  15596  psrvscafval  16135  psrridm  16149  resspsrbas  16159  resspsrvsca  16162  subrgpsr  16163  ressmplbas  16200  subrgmpl  16204  ltbwe  16214  psrbag0  16235  psrbagsn  16236  subrgascl  16239  ressply1bas  16307  zrhrhm  16466  cssss  16585  basdif0  16691  baspartn  16692  eltg3  16700  fctop  16741  cctop  16743  discld  16826  mretopd  16829  restcls  16911  ordtbaslem  16918  ordtuni  16920  ordtbas2  16921  ordtbas  16922  idcn  16987  cncls  17003  cnrmi  17088  cmpsublem  17126  cmpsub  17127  tgcmp  17128  uncmp  17130  hauscmplem  17133  cmpfi  17135  1stcrestlem  17178  disllycmp  17224  dis1stc  17225  kgeni  17232  1stckgenlem  17248  prdstopn  17322  kqffn  17416  snfil  17559  filcon  17578  cfinfil  17588  ufileu  17614  filufint  17615  fixufil  17617  cfinufil  17623  ufilen  17625  fin1aufil  17627  fmf  17640  rnelfm  17648  flimclslem  17679  hauspwpwf1  17682  supnfcls  17715  flimfnfcls  17723  fclscmp  17725  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALT  17745  ptcmplem1  17746  tsmsfbas  17810  xmet0  17907  imasdsf1olem  17937  blfval  17947  blf  17961  setsmstopn  18024  dscmet  18095  isngp2  18119  nm0  18148  tngtopn  18166  nrginvrcn  18202  nmoix  18238  qdensere  18279  iccconn  18335  metdstri  18355  iccpnfcnv  18442  xrhmeo  18444  lebnumlem3  18461  cphsubrglem  18613  tchcph  18667  cmetss  18740  bcthlem5  18750  minveclem3b  18792  cniccbdd  18821  ovolicc2lem4  18879  iunmbl  18910  ioorinv  18931  ioorcl  18932  uniioombllem2  18938  i1f1lem  19044  limcvallem  19221  ellimc2  19227  limccnp  19241  limccnp2  19242  limcco  19243  perfdvf  19253  recnprss  19254  fncpn  19282  dvcmulf  19294  c1lip1  19344  lhop2  19362  dvfsumle  19368  dvfsumabs  19370  q1pcl  19541  r1pdeglt  19544  ply1remlem  19548  plyssc  19582  ulm0  19770  cxpeq0  20025  cxplea  20043  asinlem  20164  isppw2  20353  muval2  20372  dchrfi  20494  dchrpt  20506  bposlem6  20528  lgsdir2lem2  20563  lgsqr  20585  2sqlem7  20609  2sqlem11  20614  chtppilim  20624  ex-opab  20819  grpoinvf  20907  subgornss  20973  ismgm  20987  rngomndo  21088  nvmid  21223  nmlnoubi  21374  hiidrcl  21674  hsn0elch  21827  ocsh  21862  shjshseli  22072  cmbr4i  22180  dfiop2  22333  kbpj  22536  nmopun  22594  adjeq0  22671  kbass2  22697  pjssdif1i  22755  pjinvari  22771  pjcmul2i  22782  pj3i  22788  stge1i  22818  stle0i  22819  sumdmdlem2  22999  dmdbr6ati  23003  dmdbr7ati  23004  ballotlemfelz  23049  feqmptdf  23228  ofoprabco  23232  xrlelttric  23250  xrge0iifcnv  23315  xrge0iif1  23320  disjdifprg  23352  iundisj2cnt  23368  xrge0tsmsbi  23383  esumcl  23413  esumcst  23436  esumpr2  23439  esumpinfval  23441  esumpcvgval  23446  ofcfn  23461  issgon  23484  pwsiga  23491  sigainb  23497  sssigagen  23506  measiuns  23544  dstfrvclim1  23678  subfacp1lem5  23715  erdszelem8  23729  kur14lem1  23737  indispcon  23765  cvmsss2  23805  umgra0  23877  relexpsucr  24026  dfpo2  24112  dfon2lem7  24145  trpredlem1  24230  wfrlem4  24259  wfrlem6  24261  wfrlem14  24269  wfrlem15  24270  frrlem6  24290  nosgnn0i  24313  nobndlem2  24347  nobndlem4  24349  nobndlem5  24350  nobndlem6  24351  brbigcup  24438  elsingles  24457  fnimage  24468  funpartfv  24483  dfrdg4  24488  altopthsn  24495  elaltxp  24509  axcgrtr  24543  axsegconlem9  24553  axlowdimlem5  24574  axlowdimlem17  24586  axlowdim1  24587  ellines  24775  linethru  24776  rankeq1o  24801  elhf2  24805  hfninf  24816  limsucncmpi  24884  dvreasin  24923  ump  25046  scprefat  25071  scprefat2  25072  imfstnrelc  25081  npincppr  25159  cbicp  25166  valcurfn1  25204  preoref22  25229  posprsr  25240  defge3  25271  inposet  25278  dispos  25287  caytr  25400  svs2  25487  svs3  25488  oibbi1  25509  oibbi2  25510  intopcoaconlem3b  25538  intopcoaconlem3  25539  bwt2  25592  cntrset  25602  catsbc  25849  tartarmap  25888  rocatval2  25960  cmpmorfun  25971  fnckle  26045  pfsubkl  26047  pgapspf  26052  segline  26141  segray  26155  rayline  26156  nn0prpwlem  26238  fneref  26284  refref  26285  neibastop2lem  26309  sdclem2  26452  sstotbnd2  26498  isbnd3  26508  ssbnd  26512  grpokerinj  26575  isdrngo1  26587  prtlem12  26735  elrfirn  26770  ismrcd1  26773  istopclsd  26775  rabren3dioph  26898  jm2.17b  27048  jm2.22  27088  jm2.23  27089  ttac  27129  pw2f1ocnv  27130  dnnumch1  27141  ellspd  27254  hbtlem5  27332  mncn0  27344  aaitgo  27367  rngunsnply  27378  en2eleq  27381  pmtrfmvdn0  27403  symggen  27411  psgnunilem1  27416  ssrecnpr  27537  seff  27538  sblpnf  27539  dvconstbi  27551  ipo0  27652  ifr0  27653  addrfn  27677  subrfn  27678  mulvfn  27679  refsum2cnlem1  27708  stoweidlem50  27799  stoweidlem57  27806  prelpw  28074  usisuslgra  28113  usgra0  28116  usgra0v  28117  usgra1v  28126  cusgra1v  28157  uvtx01vtx  28164  frgra0v  28174  frgra1v  28176  1vwmgra  28181  bnj145  28755  bnj216  28760  bnj1143  28822  bnj151  28909  bnj517  28917  bnj970  28979  bnj1014  28992  bnj1145  29023  bnj1498  29091  ax12-4  29106  lkrscss  29288  islshpkrN  29310  isline  29928  ispointN  29931  0psubN  29938  linepsubN  29941  atpsubN  29942  cdlemk36  31102  diafn  31224  dibfna  31344  dibvalrel  31353  dicvalrelN  31375  diclspsn  31384  dihvalrel  31469  dih1  31476  lclkrlem1  31696  lclkr  31723  mapd1o  31838  mapdin  31852  hdmapfnN  32022  hgmapfnN  32081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator