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  1980  euequ1  2342  eqssi  3324  dtru  4350  opnzi  4393  so0  4496  we0  4537  ord0  4593  ordon  4722  omssnlim  4818  funi  5442  funcnvsn  5455  fnresi  5521  fn0  5523  f0  5586  fconst  5588  f10  5668  f1o0  5671  f1oi  5672  f1osn  5674  isoid  6008  fo1st  6325  fo2nd  6326  difxp  6339  porpss  6485  iordsmo  6578  tfrlem7  6603  tfr1  6617  frfnom  6651  seqomlem2  6667  oawordeulem  6756  mapsnf1o2  7020  canth2  7219  unfilem2  7331  cantnfvalf  7576  cnfcom3clem  7618  tc2  7637  r111  7657  rankf  7676  cardf2  7786  harcard  7821  r0weon  7850  infxpenc  7855  infxpenc2lem1  7856  alephon  7906  alephf1  7922  alephiso  7935  alephsmo  7939  alephf1ALT  7940  alephfplem4  7944  ackbij1lem17  8072  ackbij1  8074  ackbij2  8079  isfin1-3  8222  fin1a2lem2  8237  fin1a2lem4  8239  axcc2lem  8272  iunfo  8370  smobeth  8417  0tsk  8586  1pi  8716  nqerf  8763  axaddf  8976  axmulf  8977  axicn  8981  mulnzcnopr  9624  negiso  9940  dfnn2  9969  nnind  9974  0z  10249  dfuzi  10316  cnref1o  10563  elrpii  10571  injresinj  11155  om2uzf1oi  11248  om2uzisoi  11249  uzrdgfni  11253  expcl2lem  11348  expclzlem  11360  expge0  11371  expge1  11372  faclbnd4lem1  11539  hashkf  11575  sqrf  12122  fclim  12302  fsumge0  12529  eff2  12655  reeff1  12676  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  sin01gt0  12746  egt2lt3  12760  qnnen  12768  ruc  12797  divalglem2  12870  divalglem9  12876  bitsf1  12913  sadaddlem  12933  2prm  13050  3prm  13051  1arith  13250  prmlem1a  13384  setsnid  13464  xpsff1o  13748  dmaf  14159  cdaf  14160  coapm  14181  isdrs2  14351  0pos  14366  isposi  14368  islati  14436  isclati  14497  fpwipodrs  14545  letsr  14627  frmdplusg  14754  odf  15130  efgsfo  15326  efgrelexlemb  15337  isabli  15381  mgpf  15630  prdscrngd  15674  xrs1cmn  16693  xrge0subm  16694  rege0subm  16710  zrngunit  16720  zlpir  16726  zzngim  16788  pjpm  16890  istpsi  16964  0cmp  17411  cmpfi  17425  indiscon  17434  kqf  17732  ptcmpfi  17798  fbssfi  17822  zfbas  17881  alexsubALTlem2  18032  alexsubALTlem4  18034  ptcmplem2  18037  ptcmp  18042  prdstmdd  18106  tsmsfbas  18110  ismeti  18308  prdsxmslem2  18512  retpsOLD  18751  cnfldms  18763  cnnrg  18768  tgqioo  18784  xrtgioo  18790  recld2  18798  xrge0gsumle  18817  xrge0tsms  18818  addcnlem  18847  divcn  18851  abscncf  18884  recncf  18885  imcncf  18886  cjcncf  18887  icopnfhmeo  18921  xrhmeo  18924  cnllycmp  18934  cncms  19262  ovolf  19331  ovolicc1  19365  ovolre  19374  ioorf  19418  opnmblALT  19448  itg2const2  19586  itg2splitlem  19593  itg2split  19594  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  iblss  19649  itgle  19654  itgeqa  19658  ibladdlem  19664  itgaddlem1  19667  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem1  19676  bddmulibl  19683  itggt0  19686  itgcn  19687  dveflem  19816  mdegxrf  19944  iaa  20195  ulmdm  20262  dvradcnv  20290  reeff1o  20316  reefiso  20317  reefgim  20319  recosf1o  20390  efifo  20402  logcn  20491  cxpcn3  20585  resqrcn  20586  ressatans  20727  efrlim  20761  efnnfsumcl  20838  efchtdvds  20895  ppiub  20941  lgslem2  21034  lgsfcl2  21039  lgsne0  21070  padicabvf  21278  usgraexvlem  21367  wlkntrllem2  21513  umgrabi  21658  konigsberg  21662  ex-pss  21689  ex-fl  21708  isgrpoi  21739  grporn  21753  isabloi  21829  issubgoi  21851  ablomul  21896  mulid  21897  cnrngo  21944  smcnlem  22146  lnocoi  22211  cncph  22273  cnbn  22324  cnchl  22371  norm3adifii  22603  hhph  22633  hhhl  22659  hlim0  22691  hlimf  22693  helch  22699  hsn0elch  22703  hhssnv  22717  hhshsslem2  22721  hhssbn  22733  hhsshl  22734  shscli  22772  shintcli  22784  chintcli  22786  shsval2i  22842  pjhthlem2  22847  lejdii  22993  nonbooli  23106  pjrni  23157  pjfoi  23158  pjfi  23159  pjmf1  23171  df0op2  23208  idunop  23434  0cnop  23435  0cnfn  23436  idcnop  23437  idhmop  23438  0hmop  23439  0lnfn  23441  0bdop  23449  lnophsi  23457  lnopcoi  23459  lnopunii  23468  lnophmi  23474  nmcopex  23485  nmcoplb  23486  nmcfnex  23509  nmcfnlb  23510  imaelshi  23514  nlelshi  23516  nlelchi  23517  riesz4i  23519  riesz4  23520  riesz1  23521  cnlnadjlem6  23528  cnlnadjlem9  23531  cnlnadjeui  23533  cnlnadjeu  23534  nmopadji  23546  bdophsi  23552  bdopcoi  23554  nmopcoadji  23557  pjhmopi  23602  pjbdlni  23605  hmopidmchi  23607  mdslj1i  23775  rinvf1o  23995  xrstos  24154  xrsclat  24155  xrge00  24161  xrge0tsmsd  24176  retos  24231  refld  24232  xrge0iifmhm  24278  xrge0pluscn  24279  qqhval2lem  24318  rnlogblem  24352  logb1  24356  esum0  24397  esumcst  24408  esumpcvgval  24421  esumcvg  24429  dmvlsiga  24465  measdivcstOLD  24531  coinfliprv  24693  ballotlem2  24699  ballotlemfc0  24703  ballotlemfcc  24704  lgamcvg2  24792  lgam1  24801  gam1  24802  indispcon  24874  cnllyscon  24885  rellyscon  24891  ghomsn  25052  soseq  25468  wfrlem11  25480  wfr1  25486  frrlem5c  25501  bdayfo  25543  bdayfn  25547  brbigcup  25652  fobigcup  25654  brsingle  25670  fnsingle  25672  brimage  25679  funimage  25681  fnimage  25682  imageval  25683  brcart  25685  brapply  25691  brcup  25692  brcap  25693  funpartfun  25696  axlowdimlem16  25800  axlowdimlem17  25801  onsucconi  26091  onsucsuccmpi  26097  mblfinlem  26143  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem1  26162  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem1  26170  bddiblnc  26174  itggt0cn  26176  areacirc  26187  comppfsc  26277  0totbnd  26372  heiborlem6  26415  mzpclall  26674  jm2.20nn  26958  dfacbasgrp  27141  dgraaf  27220  cnmsgngrp  27304  iso0  27404  dvsid  27416  abnotbtaxb  27751  bnj906  29007  ax12olem4wAUX7  29164  ax12olem4OLD7  29391  isopiN  29664  isolatiN  29699  isomliN  29722  ishlatiN  29838
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