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  1925  nfabd2  2450  dedhb  2948  sbceqal  3055  ssdifeq0  3549  r19.2zb  3557  dedth  3619  pwidg  3650  elpr2  3672  snidg  3678  ifpr  3694  prid1g  3745  pwpw0  3779  sssn  3788  preqr1  3802  pwsnALT  3838  unimax  3877  intmin3  3906  syl6eqbr  4076  intabs  4188  pwnss  4192  0inp0  4198  copsexg  4268  euotd  4283  elopab  4288  epelg  4322  ord0eln0  4462  sucidg  4486  nsuceq0  4488  onun2i  4524  fr3nr  4587  onprc  4592  ordeleqon  4596  onint0  4603  0elsuc  4642  onuninsuci  4647  orduninsuc  4650  ordzsl  4652  onzsl  4653  tfinds  4666  limomss  4677  limom  4687  peano5  4695  elvvuni  4766  posn  4774  frsn  4776  eqrelriv  4796  relopabi  4827  opabid2  4831  ididg  4853  iss  5014  dmxpss  5123  xpexr  5130  iotassuni  5251  funopg  5302  fn0  5379  f00  5442  f1o00  5524  fo00  5525  brprcneu  5534  dffn5  5584  fsn  5712  fconstfv  5750  eufnfv  5768  f1eqcocnv  5821  oprabid  5898  elrnmpt2  5973  ov6g  6001  ovelrn  6012  caovmo  6073  offn  6105  caofinvl  6120  eqop2  6179  1stconst  6223  2ndconst  6224  dftpos3  6268  dftpos4  6269  nfriotad  6329  riotaprop  6344  riotasvdOLD  6364  riotasv2d  6365  riotasv2dOLD  6366  riotasv3dOLD  6370  oawordeulem  6568  omwordi  6585  omwordri  6586  nnmwordi  6649  riiner  6748  ecopover  6778  map0e  6821  map0g  6823  mapsn  6825  elixpsn  6871  en0  6940  en1  6944  fiprc  6958  sbthlem2  6988  sbthlem4  6990  sbthlem5  6991  fodomr  7028  nneneq  7060  sdom1  7078  fineqvlem  7093  findcard  7113  findcard2  7114  fipwuni  7195  fipwss  7198  elfiun  7199  marypha1lem  7202  ordtypelem6  7254  oicl  7260  oif  7261  oion  7267  hartogslem1  7273  hartogs  7275  card2on  7284  0wdom  7300  brwdom2  7303  sucprcreg  7329  inf3lemd  7344  inf3lem6  7350  noinfepOLD  7377  cantnfle  7388  cantnflem2  7408  cantnflem3  7409  cantnflem4  7410  wemapwe  7416  cnfcom  7419  tctr  7441  r1tr  7464  r1rankidb  7492  r1pw  7533  scottex  7571  scott0  7572  bnd2  7579  tskwe  7599  oncard  7609  cardlim  7621  harsdom  7644  dfac8alem  7672  cardaleph  7732  iunfictbso  7757  infmap2  7860  ackbij1lem18  7879  cff  7890  cfub  7891  cflecard  7895  cfle  7896  cfsuc  7899  cff1  7900  cflim2  7905  cfss  7907  sdom2en01  7944  infpssrlem4  7948  fin23lem7  7958  fin23lem11  7959  isfin2-2  7961  fin23lem26  7967  fin23lem19  7978  fin23lem17  7980  fin23lem29  7983  compsscnvlem  8012  isf34lem2  8015  isf34lem4  8019  fin1a2lem6  8047  fin1a2lem10  8051  fin1a2lem12  8053  itunifn  8059  itunitc1  8062  hsmexlem1  8068  axcc2lem  8078  dcomex  8089  axdc3lem4  8095  ondomon  8201  konigthlem  8206  pwcfsdom  8221  cfpwsdom  8222  axpowndlem3  8237  canth4  8285  canthnumlem  8286  canthwelem  8288  canthwe  8289  canthp1lem2  8291  pwfseqlem4  8300  pwfseqlem5  8301  gchaleph  8313  gch2  8317  winainflem  8331  0tsk  8393  rankcf  8415  tskcard  8419  gruina  8456  grur1a  8457  grutsk  8460  tskmid  8478  indpi  8547  nqereu  8569  mulcanenq  8600  recmulnq  8604  archnq  8620  ltsopr  8672  1ne0sr  8734  0idsr  8735  00sr  8737  leid  8932  lelttric  8943  divcan3  9464  lemul1a  9626  nn1suc  9783  nn0ind-raph  10128  elnn1uz2  10310  indstr2  10312  uzsupss  10326  rpnnen1lem4  10361  rpnnen1lem5  10362  xrnemnf  10476  xrnepnf  10477  mnfltxr  10482  xrlttri  10489  xrlttr  10490  xrleid  10500  qbtwnxr  10543  xmullem2  10601  xlemul1a  10624  xrub  10646  ixxun  10688  fztpval  10861  fseq1p1m1  10873  ltweuz  11040  fzfi  11050  ser0f  11115  0exp  11153  faclbnd4lem1  11322  bcn1  11341  hashmap  11403  hashpw  11404  hashf1  11411  fz1isolem  11415  swrdlen  11472  cats1un  11492  wrdind  11493  sqr0lem  11742  sqrsq  11771  fsumrev  12257  fsumshft  12258  egt2lt3  12500  0dvds  12565  bitsp1o  12640  sadcaddlem  12664  sadcl  12669  smupvallem  12690  smucl  12691  gcddvds  12710  bezout  12737  1nprm  12779  prmind2  12785  rpdvds  12819  pcpre1  12911  vdwapf  13035  vdwapid1  13038  ram0  13085  ramz  13088  prmlem0  13123  strfvss  13182  strle1  13255  restsspw  13352  prdsless  13378  prdsdsfn  13380  imasdsfn  13433  imasaddfnlem  13446  imasvscafn  13455  xpscfv  13480  xpsfrnel  13481  isacs1i  13575  cidfn  13597  comffn  13624  isoval  13683  sscres  13716  cofucl  13778  idffth  13823  ressffth  13828  catcoppccl  13956  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  curfcl  14022  hofcl  14049  yonedainv  14071  pospo  14123  ipopos  14279  acsficl2d  14295  dirref  14373  mgmidcl  14404  mgmlrid  14405  symggrp  14796  symgid  14797  cntzssv  14820  slwpgp  14940  frgpmhm  15090  frgpuptinv  15096  frgpup3lem  15102  gsumcom2  15242  abv0  15612  psrvscafval  16151  psrridm  16165  resspsrbas  16175  resspsrvsca  16178  subrgpsr  16179  ressmplbas  16216  subrgmpl  16220  ltbwe  16230  psrbag0  16251  psrbagsn  16252  subrgascl  16255  ressply1bas  16323  zrhrhm  16482  cssss  16601  basdif0  16707  baspartn  16708  eltg3  16716  fctop  16757  cctop  16759  discld  16842  mretopd  16845  restcls  16927  ordtbaslem  16934  ordtuni  16936  ordtbas2  16937  ordtbas  16938  idcn  17003  cncls  17019  cnrmi  17104  cmpsublem  17142  cmpsub  17143  tgcmp  17144  uncmp  17146  hauscmplem  17149  cmpfi  17151  1stcrestlem  17194  disllycmp  17240  dis1stc  17241  kgeni  17248  1stckgenlem  17264  prdstopn  17338  kqffn  17432  snfil  17575  filcon  17594  cfinfil  17604  ufileu  17630  filufint  17631  fixufil  17633  cfinufil  17639  ufilen  17641  fin1aufil  17643  fmf  17656  rnelfm  17664  flimclslem  17695  hauspwpwf1  17698  supnfcls  17731  flimfnfcls  17739  fclscmp  17741  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALT  17761  ptcmplem1  17762  tsmsfbas  17826  xmet0  17923  imasdsf1olem  17953  blfval  17963  blf  17977  setsmstopn  18040  dscmet  18111  isngp2  18135  nm0  18164  tngtopn  18182  nrginvrcn  18218  nmoix  18254  qdensere  18295  iccconn  18351  metdstri  18371  iccpnfcnv  18458  xrhmeo  18460  lebnumlem3  18477  cphsubrglem  18629  tchcph  18683  cmetss  18756  bcthlem5  18766  minveclem3b  18808  cniccbdd  18837  ovolicc2lem4  18895  iunmbl  18926  ioorinv  18947  ioorcl  18948  uniioombllem2  18954  i1f1lem  19060  limcvallem  19237  ellimc2  19243  limccnp  19257  limccnp2  19258  limcco  19259  perfdvf  19269  recnprss  19270  fncpn  19298  dvcmulf  19310  c1lip1  19360  lhop2  19378  dvfsumle  19384  dvfsumabs  19386  q1pcl  19557  r1pdeglt  19560  ply1remlem  19564  plyssc  19598  ulm0  19786  cxpeq0  20041  cxplea  20059  asinlem  20180  isppw2  20369  muval2  20388  dchrfi  20510  dchrpt  20522  bposlem6  20544  lgsdir2lem2  20579  lgsqr  20601  2sqlem7  20625  2sqlem11  20630  chtppilim  20640  ex-opab  20835  grpoinvf  20923  subgornss  20989  ismgm  21003  rngomndo  21104  nvmid  21239  nmlnoubi  21390  hiidrcl  21690  hsn0elch  21843  ocsh  21878  shjshseli  22088  cmbr4i  22196  dfiop2  22349  kbpj  22552  nmopun  22610  adjeq0  22687  kbass2  22713  pjssdif1i  22771  pjinvari  22787  pjcmul2i  22798  pj3i  22804  stge1i  22834  stle0i  22835  sumdmdlem2  23015  dmdbr6ati  23019  dmdbr7ati  23020  ballotlemfelz  23065  feqmptdf  23243  ofoprabco  23247  xrlelttric  23265  xrge0iifcnv  23330  xrge0iif1  23335  disjdifprg  23367  iundisj2cnt  23383  xrge0tsmsbi  23398  esumcl  23428  esumcst  23451  esumpr2  23454  esumpinfval  23456  esumpcvgval  23461  ofcfn  23476  issgon  23499  pwsiga  23506  sigainb  23512  sssigagen  23521  measiuns  23559  dstfrvclim1  23693  subfacp1lem5  23730  erdszelem8  23744  kur14lem1  23752  indispcon  23780  cvmsss2  23820  umgra0  23892  relexpsucr  24041  prodf1f  24166  dfpo2  24183  dfon2lem7  24216  trpredlem1  24301  wfrlem4  24330  wfrlem6  24332  wfrlem14  24340  wfrlem15  24341  frrlem6  24361  nosgnn0i  24384  nobndlem2  24418  nobndlem4  24420  nobndlem5  24421  nobndlem6  24422  brbigcup  24509  elsingles  24528  fnimage  24539  funpartlem  24552  dfrdg4  24560  altopthsn  24567  elaltxp  24581  axcgrtr  24615  axsegconlem9  24625  axlowdimlem5  24646  axlowdimlem17  24658  axlowdim1  24659  ellines  24847  linethru  24848  rankeq1o  24873  elhf2  24877  hfninf  24888  limsucncmpi  24956  dvreasin  25026  ump  25149  scprefat  25174  scprefat2  25175  imfstnrelc  25184  npincppr  25262  cbicp  25269  valcurfn1  25307  preoref22  25332  posprsr  25343  defge3  25374  inposet  25381  dispos  25390  caytr  25503  svs2  25590  svs3  25591  oibbi1  25612  oibbi2  25613  intopcoaconlem3b  25641  intopcoaconlem3  25642  bwt2  25695  cntrset  25705  catsbc  25952  tartarmap  25991  rocatval2  26063  cmpmorfun  26074  fnckle  26148  pfsubkl  26150  pgapspf  26155  segline  26244  segray  26258  rayline  26259  nn0prpwlem  26341  fneref  26387  refref  26388  neibastop2lem  26412  sdclem2  26555  sstotbnd2  26601  isbnd3  26611  ssbnd  26615  grpokerinj  26678  isdrngo1  26690  prtlem12  26838  elrfirn  26873  ismrcd1  26876  istopclsd  26878  rabren3dioph  27001  jm2.17b  27151  jm2.22  27191  jm2.23  27192  ttac  27232  pw2f1ocnv  27233  dnnumch1  27244  ellspd  27357  hbtlem5  27435  mncn0  27447  aaitgo  27470  rngunsnply  27481  en2eleq  27484  pmtrfmvdn0  27506  symggen  27514  psgnunilem1  27519  ssrecnpr  27640  seff  27641  sblpnf  27642  dvconstbi  27654  ipo0  27755  ifr0  27756  addrfn  27780  subrfn  27781  mulvfn  27782  refsum2cnlem1  27811  stoweidlem50  27902  stoweidlem57  27909  prelpw  28184  hashgt12el2  28219  usisuslgra  28247  usgra0  28250  usgra0v  28251  usgra1v  28260  nb3graprlem1  28287  cusgra1v  28296  uvtx01vtx  28305  wlkntrl  28350  0spth  28357  3v3e3cycl1  28390  constr3trllem1  28396  constr3pthlem3  28403  4cycl4v4e  28412  4cycl4dv  28413  frgra0v  28420  frgra1v  28422  1vwmgra  28427  bnj145  29071  bnj216  29076  bnj1143  29138  bnj151  29225  bnj517  29233  bnj970  29295  bnj1014  29308  bnj1145  29339  bnj1498  29407  nfald2OLD7  29671  ax12-4  29728  lkrscss  29910  islshpkrN  29932  isline  30550  ispointN  30553  0psubN  30560  linepsubN  30563  atpsubN  30564  cdlemk36  31724  diafn  31846  dibfna  31966  dibvalrel  31975  dicvalrelN  31997  diclspsn  32006  dihvalrel  32091  dih1  32098  lclkrlem1  32318  lclkr  32345  mapd1o  32460  mapdin  32474  hdmapfnN  32644  hgmapfnN  32703
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