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

Theorem mpbir2an 888
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 886 . 2  |-  ( ph  <->  ch )
51, 4mpbir 202 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  3pm3.2i  1132  ax12olem4  1873  euequ1  2233  eqssi  3197  dtru  4201  opnzi  4243  so0  4347  we0  4388  ord0  4444  ordon  4574  omssnlim  4670  funi  5251  funcnvsn  5263  fnresi  5327  fn0  5329  f0  5391  fconst  5393  f10  5473  f1o0  5476  f1oi  5477  f1osn  5479  isoid  5788  fo1st  6101  fo2nd  6102  difxp  6115  porpss  6243  iordsmo  6370  tfrlem7  6395  tfr1  6409  frfnom  6443  seqomlem2  6459  oawordeulem  6548  mapsnf1o2  6811  canth2  7010  unfilem2  7118  cantnfvalf  7362  cnfcom3clem  7404  tc2  7423  r111  7443  rankf  7462  cardf2  7572  harcard  7607  r0weon  7636  infxpenc  7641  infxpenc2lem1  7642  alephon  7692  alephf1  7708  alephiso  7721  alephsmo  7725  alephf1ALT  7726  alephfplem4  7730  ackbij1lem17  7858  ackbij1  7860  ackbij2  7865  isfin1-3  8008  fin1a2lem2  8023  fin1a2lem4  8025  axcc2lem  8058  iunfo  8157  smobeth  8204  0tsk  8373  1pi  8503  nqerf  8550  axaddf  8763  axmulf  8764  axicn  8768  mulnzcnopr  9410  negiso  9726  dfnn2  9755  nnind  9760  0z  10031  dfuzi  10098  cnref1o  10345  elrpii  10353  om2uzf1oi  11011  om2uzisoi  11012  uzrdgfni  11016  expcl2lem  11110  expclzlem  11122  expge0  11133  expge1  11134  faclbnd4lem1  11301  hashkf  11334  sqrf  11842  fclim  12022  fsumge0  12248  eff2  12374  reeff1  12395  ef01bndlem  12459  sin01bnd  12460  cos01bnd  12461  sin01gt0  12465  egt2lt3  12479  qnnen  12487  ruc  12516  divalglem2  12589  divalglem9  12595  bitsf1  12632  sadaddlem  12652  2prm  12769  3prm  12770  1arith  12969  prmlem1a  13103  setsnid  13183  xpsff1o  13465  dmaf  13876  cdaf  13877  coapm  13898  isdrs2  14068  0pos  14083  isposi  14085  islati  14153  isclati  14214  fpwipodrs  14262  letsr  14344  frmdplusg  14471  odf  14847  efgsfo  15043  efgrelexlemb  15054  isabli  15098  mgpf  15347  prdscrngd  15391  xrs1cmn  16406  xrge0subm  16407  rege0subm  16423  zrngunit  16433  zlpir  16439  zzngim  16501  pjpm  16603  istpsi  16677  0cmp  17116  cmpfi  17130  indiscon  17139  kqf  17433  ptcmpfi  17499  fbssfi  17527  zfbas  17586  alexsubALTlem2  17737  alexsubALTlem4  17739  ptcmplem2  17742  ptcmp  17747  prdstmdd  17801  tsmsfbas  17805  ismeti  17885  prdsxmslem2  18070  retpsOLD  18268  cnfldms  18280  cnnrg  18285  tgqioo  18301  xrtgioo  18307  recld2  18315  xrge0gsumle  18333  xrge0tsms  18334  addcnlem  18363  divcn  18367  abscncf  18400  recncf  18401  imcncf  18402  cjcncf  18403  icopnfhmeo  18436  xrhmeo  18439  cnllycmp  18449  cncms  18769  ovolf  18836  ovolicc1  18870  ovolre  18879  ioorf  18923  opnmblALT  18953  itg2const2  19091  itg2splitlem  19098  itg2split  19099  itg2gt0  19110  itg2cnlem1  19111  itg2cnlem2  19112  itg2cn  19113  iblss  19154  itgle  19159  itgeqa  19163  ibladdlem  19169  itgaddlem1  19172  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgmulc2lem1  19181  bddmulibl  19188  itggt0  19191  itgcn  19192  dveflem  19321  mdegxrf  19449  iaa  19700  dvradcnv  19792  reeff1o  19818  reefiso  19819  reefgim  19821  recosf1o  19892  efifo  19904  logcn  19989  cxpcn3  20083  resqrcn  20084  ressatans  20225  efrlim  20259  efnnfsumcl  20335  efchtdvds  20392  ppiub  20438  lgslem2  20531  lgsfcl2  20536  lgsne0  20567  padicabvf  20775  ex-pss  20791  ex-fl  20810  isgrpoi  20858  grporn  20872  isabloi  20948  issubgoi  20970  ablomul  21015  mulid  21016  cnrngo  21063  smcnlem  21263  lnocoi  21328  cncph  21390  cnbn  21441  cnchl  21488  norm3adifii  21720  hhph  21750  hhhl  21776  hlim0  21808  hlimf  21810  helch  21816  hsn0elch  21820  hhssnv  21834  hhshsslem2  21838  hhssbn  21850  hhsshl  21851  shscli  21889  shintcli  21901  chintcli  21903  shsval2i  21959  pjhthlem2  21964  lejdii  22110  nonbooli  22223  pjrni  22274  pjfoi  22275  pjfi  22276  pjmf1  22288  df0op2  22325  idunop  22551  0cnop  22552  0cnfn  22553  idcnop  22554  idhmop  22555  0hmop  22556  0lnfn  22558  0bdop  22566  lnophsi  22574  lnopcoi  22576  lnopunii  22585  lnophmi  22591  nmcopex  22602  nmcoplb  22603  nmcfnex  22626  nmcfnlb  22627  imaelshi  22631  nlelshi  22633  nlelchi  22634  riesz4i  22636  riesz4  22637  riesz1  22638  cnlnadjlem6  22645  cnlnadjlem9  22648  cnlnadjeui  22650  cnlnadjeu  22651  nmopadji  22663  bdophsi  22669  bdopcoi  22671  nmopcoadji  22674  pjhmopi  22719  pjbdlni  22722  hmopidmchi  22724  mdslj1i  22892  indispcon  23170  cnllyscon  23181  rellyscon  23187  umgrabi  23312  konigsberg  23316  ghomsn  23400  soseq  23656  wfrlem11  23668  wfr1  23674  frrlem5c  23689  axbday  23730  bdayfn  23734  brbigcup  23847  fobigcup  23849  brsingle  23864  fnsingle  23866  brimage  23873  funimage  23875  fnimage  23876  imageval  23877  brcart  23879  brapply  23885  brcup  23886  brcap  23887  funpartfun  23889  axlowdimlem16  23993  axlowdimlem17  23994  onsucconi  24284  onsucsuccmpi  24290  vxveqv  24453  zintdom  24838  indcomp  24989  1alg  25122  1ded  25138  0alg  25156  0ded  25157  0catOLD  25158  1cat  25159  pgapspf  25452  comppfsc  25707  0totbnd  25897  heiborlem6  25940  mzpclall  26205  jm2.20nn  26490  dfacbasgrp  26673  dgraaf  26752  cnmsgngrp  26836  iso0  26936  dvsid  26948  bnj906  28230  isopiN  28639  isolatiN  28674  isomliN  28697  ishlatiN  28813
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator