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

Theorem mpbir2an 887
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
Ref Expression
mpbir2an.1  |-  ps
mpbir2an.2  |-  ch
mpbiran2an.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbir2an  |-  ph

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2  |-  ch
2 mpbir2an.1 . . 3  |-  ps
3 mpbiran2an.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
42, 3mpbiran 885 . 2  |-  ( ph  <->  ch )
51, 4mpbir 201 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  3pm3.2i  1132  ax12olem4OLD  1968  euequ1  2326  eqssi  3307  dtru  4331  opnzi  4374  so0  4477  we0  4518  ord0  4574  ordon  4703  omssnlim  4799  funi  5423  funcnvsn  5436  fnresi  5502  fn0  5504  f0  5567  fconst  5569  f10  5649  f1o0  5652  f1oi  5653  f1osn  5655  isoid  5988  fo1st  6305  fo2nd  6306  difxp  6319  porpss  6462  iordsmo  6555  tfrlem7  6580  tfr1  6594  frfnom  6628  seqomlem2  6644  oawordeulem  6733  mapsnf1o2  6997  canth2  7196  unfilem2  7308  cantnfvalf  7553  cnfcom3clem  7595  tc2  7614  r111  7634  rankf  7653  cardf2  7763  harcard  7798  r0weon  7827  infxpenc  7832  infxpenc2lem1  7833  alephon  7883  alephf1  7899  alephiso  7912  alephsmo  7916  alephf1ALT  7917  alephfplem4  7921  ackbij1lem17  8049  ackbij1  8051  ackbij2  8056  isfin1-3  8199  fin1a2lem2  8214  fin1a2lem4  8216  axcc2lem  8249  iunfo  8347  smobeth  8394  0tsk  8563  1pi  8693  nqerf  8740  axaddf  8953  axmulf  8954  axicn  8958  mulnzcnopr  9600  negiso  9916  dfnn2  9945  nnind  9950  0z  10225  dfuzi  10292  cnref1o  10539  elrpii  10547  injresinj  11127  om2uzf1oi  11220  om2uzisoi  11221  uzrdgfni  11225  expcl2lem  11320  expclzlem  11332  expge0  11343  expge1  11344  faclbnd4lem1  11511  hashkf  11547  sqrf  12094  fclim  12274  fsumge0  12501  eff2  12627  reeff1  12648  ef01bndlem  12712  sin01bnd  12713  cos01bnd  12714  sin01gt0  12718  egt2lt3  12732  qnnen  12740  ruc  12769  divalglem2  12842  divalglem9  12848  bitsf1  12885  sadaddlem  12905  2prm  13022  3prm  13023  1arith  13222  prmlem1a  13356  setsnid  13436  xpsff1o  13720  dmaf  14131  cdaf  14132  coapm  14153  isdrs2  14323  0pos  14338  isposi  14340  islati  14408  isclati  14469  fpwipodrs  14517  letsr  14599  frmdplusg  14726  odf  15102  efgsfo  15298  efgrelexlemb  15309  isabli  15353  mgpf  15602  prdscrngd  15646  xrs1cmn  16661  xrge0subm  16662  rege0subm  16678  zrngunit  16688  zlpir  16694  zzngim  16756  pjpm  16858  istpsi  16932  0cmp  17379  cmpfi  17393  indiscon  17402  kqf  17700  ptcmpfi  17766  fbssfi  17790  zfbas  17849  alexsubALTlem2  18000  alexsubALTlem4  18002  ptcmplem2  18005  ptcmp  18010  prdstmdd  18074  tsmsfbas  18078  ismeti  18264  prdsxmslem2  18449  retpsOLD  18669  cnfldms  18681  cnnrg  18686  tgqioo  18702  xrtgioo  18708  recld2  18716  xrge0gsumle  18735  xrge0tsms  18736  addcnlem  18765  divcn  18769  abscncf  18802  recncf  18803  imcncf  18804  cjcncf  18805  icopnfhmeo  18839  xrhmeo  18842  cnllycmp  18852  cncms  19176  ovolf  19245  ovolicc1  19279  ovolre  19288  ioorf  19332  opnmblALT  19362  itg2const2  19500  itg2splitlem  19507  itg2split  19508  itg2gt0  19519  itg2cnlem1  19520  itg2cnlem2  19521  itg2cn  19522  iblss  19563  itgle  19568  itgeqa  19572  ibladdlem  19578  itgaddlem1  19581  iblabslem  19586  iblabs  19587  iblabsr  19588  iblmulc2  19589  itgmulc2lem1  19590  bddmulibl  19597  itggt0  19600  itgcn  19601  dveflem  19730  mdegxrf  19858  iaa  20109  ulmdm  20176  dvradcnv  20204  reeff1o  20230  reefiso  20231  reefgim  20233  recosf1o  20304  efifo  20316  logcn  20405  cxpcn3  20499  resqrcn  20500  ressatans  20641  efrlim  20675  efnnfsumcl  20752  efchtdvds  20809  ppiub  20855  lgslem2  20948  lgsfcl2  20953  lgsne0  20984  padicabvf  21192  usgraexvlem  21280  wlkntrllem4  21416  umgrabi  21553  konigsberg  21557  ex-pss  21584  ex-fl  21603  isgrpoi  21634  grporn  21648  isabloi  21724  issubgoi  21746  ablomul  21791  mulid  21792  cnrngo  21839  smcnlem  22041  lnocoi  22106  cncph  22168  cnbn  22219  cnchl  22266  norm3adifii  22498  hhph  22528  hhhl  22554  hlim0  22586  hlimf  22588  helch  22594  hsn0elch  22598  hhssnv  22612  hhshsslem2  22616  hhssbn  22628  hhsshl  22629  shscli  22667  shintcli  22679  chintcli  22681  shsval2i  22737  pjhthlem2  22742  lejdii  22888  nonbooli  23001  pjrni  23052  pjfoi  23053  pjfi  23054  pjmf1  23066  df0op2  23103  idunop  23329  0cnop  23330  0cnfn  23331  idcnop  23332  idhmop  23333  0hmop  23334  0lnfn  23336  0bdop  23344  lnophsi  23352  lnopcoi  23354  lnopunii  23363  lnophmi  23369  nmcopex  23380  nmcoplb  23381  nmcfnex  23404  nmcfnlb  23405  imaelshi  23409  nlelshi  23411  nlelchi  23412  riesz4i  23414  riesz4  23415  riesz1  23416  cnlnadjlem6  23423  cnlnadjlem9  23426  cnlnadjeui  23428  cnlnadjeu  23429  nmopadji  23441  bdophsi  23447  bdopcoi  23449  nmopcoadji  23452  pjhmopi  23497  pjbdlni  23500  hmopidmchi  23502  mdslj1i  23670  rinvf1o  23885  xrge00  24037  xrge0tsmsd  24052  retos  24094  refld  24095  xrge0iifmhm  24129  xrge0pluscn  24130  qqhval2lem  24164  rnlogblem  24195  logb1  24199  esum0  24240  esumcst  24251  esumpcvgval  24264  esumcvg  24272  dmvlsiga  24308  measdivcstOLD  24372  coinfliprv  24519  ballotlem2  24525  ballotlemfc0  24529  ballotlemfcc  24530  lgamcvg2  24618  lgam1  24627  gam1  24628  indispcon  24700  cnllyscon  24711  rellyscon  24717  ghomsn  24878  soseq  25278  wfrlem11  25290  wfr1  25296  frrlem5c  25311  bdayfo  25353  bdayfn  25357  brbigcup  25462  fobigcup  25464  brsingle  25480  fnsingle  25482  brimage  25489  funimage  25491  fnimage  25492  imageval  25493  brcart  25495  brapply  25501  brcup  25502  brcap  25503  funpartfun  25506  axlowdimlem16  25610  axlowdimlem17  25611  onsucconi  25901  onsucsuccmpi  25907  itg2gt0cn  25960  ibladdnclem  25961  itgaddnclem1  25963  iblabsnclem  25968  iblabsnc  25969  iblmulc2nc  25970  itgmulc2nclem1  25971  bddiblnc  25975  itggt0cn  25977  areacirc  25988  comppfsc  26078  0totbnd  26173  heiborlem6  26216  mzpclall  26475  jm2.20nn  26759  dfacbasgrp  26942  dgraaf  27021  cnmsgngrp  27105  iso0  27205  dvsid  27217  abnotbtaxb  27552  bnj906  28639  ax12olem4wAUX7  28796  ax12olem4OLD7  29023  isopiN  29296  isolatiN  29331  isomliN  29354  ishlatiN  29470
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 178  df-an 361
  Copyright terms: Public domain W3C validator