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

Theorem mpbir2an 920
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
Ref Expression
mpbir2an.1
mpbir2an.2
mpbiran2an.1
Assertion
Ref Expression
mpbir2an

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2
2 mpbir2an.1 . . 3
3 mpbiran2an.1 . . 3
42, 3mpbiran 918 . 2
51, 4mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  3pm3.2i  1174  euequ1OLD  2387  eqssi  3519  dtru  4643  opnzi  4724  so0  4838  we0  4879  ord0  4935  difxp  5436  funi  5623  funcnvsn  5638  fnresi  5703  fn0  5705  f0  5771  fconst  5776  f10  5852  f1o0  5855  f1oi  5856  f1osn  5858  isoid  6225  porpss  6584  ordon  6618  omssnlim  6714  fo1st  6820  fo2nd  6821  iordsmo  7047  tfrlem7  7071  tfr1  7085  frfnom  7119  seqomlem2  7135  oawordeulem  7222  mapsnf1o2  7486  canth2  7690  unfilem2  7805  cantnfvalf  8105  cnfcom3clem  8170  cnfcom3clemOLD  8178  tc2  8194  r111  8214  rankf  8233  cardf2  8345  harcard  8380  r0weon  8411  infxpenc  8416  infxpenc2lem1  8417  infxpencOLD  8421  alephon  8471  alephf1  8487  alephiso  8500  alephsmo  8504  alephf1ALT  8505  alephfplem4  8509  ackbij1lem17  8637  ackbij1  8639  ackbij2  8644  isfin1-3  8787  fin1a2lem2  8802  fin1a2lem4  8804  axcc2lem  8837  iunfo  8935  smobeth  8982  0tsk  9154  1pi  9282  nqerf  9329  axaddf  9543  axmulf  9544  axicn  9548  mulnzcnopr  10220  negiso  10544  dfnn2  10574  nnind  10579  0z  10900  dfuzi  10978  cnref1o  11244  elrpii  11252  0e0icopnf  11659  0e0iccpnf  11660  om2uzf1oi  12064  om2uzisoi  12065  uzrdgfni  12069  expcl2lem  12178  expclzlem  12190  expge0  12202  expge1  12203  faclbnd4lem1  12371  hashkf  12407  wwlktovf1  12895  sqrtf  13196  fclim  13376  eff2  13834  reeff1  13855  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  sin01gt0  13925  egt2lt3  13939  qnnen  13947  ruc  13976  divalglem2  14053  divalglem9  14059  bitsf1  14096  sadaddlem  14116  2prm  14233  3prm  14234  1arith  14445  prmlem1a  14592  setsnid  14674  xpsff1o  14965  dmaf  15376  cdaf  15377  coapm  15398  isdrs2  15568  0pos  15584  isposi  15586  fpwipodrs  15794  letsr  15857  frmdplusg  16022  symg2bas  16423  pmtrsn  16544  odf  16561  efgsfo  16757  efgrelexlemb  16768  isabli  16812  mgpf  17210  prdscrngd  17262  xrsmgmdifsgrp  18455  xrs1cmn  18458  zringnzr  18500  zringlpir  18512  zlpir  18517  zringunit  18520  zrngunit  18521  zzngim  18591  cnmsgngrp  18615  psgninv  18618  zrhpsgnmhm  18620  retos  18654  refld  18655  pjpm  18739  istpsi  19445  0cmp  19894  cmpfi  19908  indiscon  19919  comppfsc  20033  kqf  20248  ptcmpfi  20314  fbssfi  20338  zfbas  20397  alexsubALTlem2  20548  alexsubALTlem4  20550  ptcmplem2  20553  ptcmp  20558  prdstmdd  20622  tsmsfbas  20626  ismeti  20828  prdsxmslem2  21032  retpsOLD  21271  cnfldms  21283  cnnrg  21288  tgqioo  21305  xrtgioo  21311  recld2  21319  xrge0gsumle  21338  xrge0tsms  21339  addcnlem  21368  divcn  21372  abscncf  21405  recncf  21406  imcncf  21407  cjcncf  21408  icopnfhmeo  21443  xrhmeo  21446  cnllycmp  21456  cncms  21795  ovolf  21893  ovolicc1  21927  ovolre  21936  ioorf  21982  opnmblALT  22012  dveflem  22380  mdegxrf  22468  iaa  22721  ulmdm  22788  dvradcnv  22816  reeff1o  22842  reefiso  22843  reefgim  22845  recosf1o  22922  efifo  22934  rzgrp  22941  logcn  23028  cxpcn3  23122  resqrtcn  23123  ressatans  23265  efnnfsumcl  23376  efchtdvds  23433  ppiub  23479  lgslem2  23572  lgsfcl2  23577  lgsne0  23608  padicabvf  23816  axlowdimlem16  24260  usgraexvlem  24395  wlkntrllem2  24562  umgrabi  24983  konigsberg  24987  ex-pss  25149  ex-fl  25168  isgrpoi  25200  grporn  25214  isabloi  25290  issubgoi  25312  ablomul  25357  mulid  25358  cnrngo  25405  smcnlem  25607  lnocoi  25672  cncph  25734  cnbn  25785  cnchl  25832  norm3adifii  26065  hhph  26095  hhhl  26121  hlim0  26153  hlimf  26155  helch  26161  hsn0elch  26166  hhssnv  26180  hhshsslem2  26184  hhssbn  26196  hhsshl  26197  shscli  26235  shintcli  26247  chintcli  26249  shsval2i  26305  pjhthlem2  26310  lejdii  26456  nonbooli  26569  pjrni  26620  pjfoi  26621  pjfi  26622  pjmf1  26634  df0op2  26671  idunop  26897  0cnop  26898  0cnfn  26899  idcnop  26900  idhmop  26901  0hmop  26902  0lnfn  26904  0bdop  26912  lnophsi  26920  lnopcoi  26922  lnopunii  26931  lnophmi  26937  nmcopex  26948  nmcoplb  26949  nmcfnex  26972  nmcfnlb  26973  imaelshi  26977  nlelshi  26979  nlelchi  26980  riesz4i  26982  riesz4  26983  riesz1  26984  cnlnadjlem6  26991  cnlnadjlem9  26994  cnlnadjeui  26996  cnlnadjeu  26997  nmopadji  27009  bdophsi  27015  bdopcoi  27017  nmopcoadji  27020  pjhmopi  27065  pjbdlni  27068  hmopidmchi  27070  mdslj1i  27238  rinvf1o  27472  nnindf  27610  xrstos  27667  xrsclat  27668  xrge0omnd  27701  xrge0tsmsd  27775  reofld  27830  nn0archi  27833  xrge0iifmhm  27921  xrge0pluscn  27922  cnzh  27951  rezh  27952  qqhval2lem  27962  logb1  28019  esum0  28060  esumcst  28071  esumpcvgval  28084  esumcvg  28092  dmvlsiga  28129  measdivcstOLD  28195  eulerpartlemt  28310  coinfliprv  28421  ballotlem2  28427  signswmnd  28514  lgamcvg2  28597  lgam1  28606  gam1  28607  indispcon  28679  cnllyscon  28690  rellyscon  28696  msrf  28902  ghomsn  29028  soseq  29334  wfrlem11  29353  wfr1  29359  frrlem5c  29393  bdayfo  29435  bdayfn  29439  brbigcup  29548  fobigcup  29550  brsingle  29567  fnsingle  29569  brimage  29576  funimage  29578  fnimage  29579  imageval  29580  brcart  29582  brapply  29588  brcup  29589  brcap  29590  funpartfun  29593  brub  29604  onsucconi  29902  onsucsuccmpi  29908  mblfinlem2  30052  areacirc  30112  0totbnd  30269  heiborlem6  30312  mzpclall  30659  jm2.20nn  30939  dfacbasgrp  31057  dgraaf  31096  iso0  31187  dvsid  31236  halffl  31493  resincncf  31677  0cnf  31679  iblempty  31764  dirkeritg  31884  fourierdlem62  31951  fourierdlem76  31965  fourierdlem103  31992  etransclem18  32035  etransclem46  32063  abnotbtaxb  32111  1odd  32499  nnsgrp  32505  0even  32737  2even  32739  2zrngamgm  32745  2zrngasgrp  32746  2zrngamnd  32747  2zrngagrp  32749  2zrngmsgrp  32753  zlmodzxzldeplem3  33103  lvecpsslmod  33108  ldepsnlinc  33109  aacllem  33216  bnj906  33988  bj-dtru  34383  bj-rabtr  34497  isolatiN  34941  isomliN  34964  ishlatiN  35080  taupilem2  37697  taupi  37698  trclub  37784  trclubg  37785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator