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

Theorem mpbir2an 710
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
Hypotheses
Ref Expression
mpbir2an.1 𝜓
mpbir2an.2 𝜒
mpbir2an.maj (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
mpbir2an 𝜑

Proof of Theorem mpbir2an
StepHypRef Expression
1 mpbir2an.2 . 2 𝜒
2 mpbir2an.1 . . 3 𝜓
3 mpbir2an.maj . . 3 (𝜑 ↔ (𝜓𝜒))
42, 3mpbiran 708 . 2 (𝜑𝜒)
51, 4mpbir 234 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  3pm3.2i  1336  equsb1vOLDOLD  2519  sbtvOLD  2521  euequ  2684  eqssi  3969  elini  4155  dtru  5259  opnzi  5354  so0  5497  we0  5538  difxp  6010  ord0  6232  dfiota4  6337  funi  6377  funcnvsn  6394  idfn  6466  fnresiOLD  6468  fn0  6470  f0  6552  fconst  6557  f10  6640  f1o0  6644  f1oi  6645  f1osn  6647  isoid  7077  porpss  7449  epweon  7493  ordon  7494  omssnlim  7590  fo1st  7706  fo2nd  7707  wfrfun  7963  wfr1  7971  iordsmo  7992  tfrlem7  8017  tfr1  8031  frfnom  8068  seqomlem2  8085  oawordeulem  8178  mapsnf1o2  8456  canth2  8669  unfilem2  8782  cantnfvalf  9127  cnfcom3clem  9167  tc2  9183  r111  9203  rankf  9222  cardf2  9371  harcard  9406  r0weon  9438  infxpenc  9444  infxpenc2lem1  9445  alephon  9495  alephf1  9511  alephiso  9524  alephsmo  9528  alephf1ALT  9529  alephfplem4  9533  ackbij1lem17  9658  ackbij1  9660  ackbij2  9665  fin1a2lem2  9823  fin1a2lem4  9825  axcc2lem  9858  iunfo  9961  smobeth  10008  0tsk  10177  1pi  10305  nqerf  10352  axaddf  10567  axmulf  10568  axicn  10572  mulnzcnopr  11286  negiso  11619  dfnn2  11649  nnind  11654  0z  11991  dfuzi  12072  cnref1o  12383  elrpii  12391  0e0icopnf  12847  0e0iccpnf  12848  fz0to4untppr  13016  fldiv4p1lem1div2  13211  om2uzf1oi  13327  om2uzisoi  13328  uzrdgfni  13332  expcl2lem  13448  expclzlem  13460  expge0  13472  expge1  13473  faclbnd4lem1  13660  hashkf  13699  wwlktovf1  14323  sqrtf  14725  fclim  14912  fprodn0f  15347  eff2  15454  reeff1  15475  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  sin01gt0  15545  egt2lt3  15561  qnnen  15568  ruc  15598  halfleoddlt  15713  divalglem2  15746  divalglem9  15752  bitsf1  15795  sadaddlem  15815  2prm  16036  3prm  16038  1arith  16263  prmlem1a  16442  setsnid  16541  xpsff1o  16842  dmaf  17311  cdaf  17312  coapm  17333  0pos  17566  isposi  17568  letsr  17839  sgrp0b  17911  frmdplusg  18021  efmndsgrp  18053  smndex1sgrp  18075  smndex1mnd  18077  symg2bas  18523  pmtrsn  18649  odf  18667  efgsfo  18867  efgrelexlemb  18878  isabli  18923  mgpf  19314  prdscrngd  19368  xrsmgmdifsgrp  20137  xrs1cmn  20140  cnmgpid  20162  zringnzr  20184  zringunit  20190  zringlpir  20191  zringndrg  20192  zzngim  20253  cnmsgngrp  20277  psgninv  20280  zrhpsgnmhm  20282  retos  20316  refld  20317  rzgrp  20321  pjpm  20406  fntopon  21538  istpsi  21556  cmpfi  22022  indisconn  22032  kqf  22361  fbssfi  22451  zfbas  22510  ptcmplem2  22667  prdstmdd  22738  tsmsfbas  22742  ismeti  22941  prdsxmslem2  23145  cnfldms  23390  cnnrg  23395  tgqioo  23414  xrtgioo  23420  recld2  23428  xrge0gsumle  23447  xrge0tsms  23448  addcnlem  23478  divcn  23482  abscncf  23515  recncf  23516  imcncf  23517  cjcncf  23518  icopnfhmeo  23557  xrhmeo  23560  cnllycmp  23570  isclmi0  23712  iscvsi  23743  cnstrcvs  23755  cncms  23968  ovolf  24095  ovolre  24138  opnmblALT  24216  dveflem  24591  mdegxrf  24678  iaa  24930  ulmdm  24997  dvradcnv  25025  reeff1o  25051  reefiso  25052  reefgim  25054  recosf1o  25136  efifo  25148  logcn  25247  cxpcn3  25346  resqrtcn  25347  logb1  25364  logbmpt  25383  2logb9irrALT  25393  sqrt2cxp2logb9e3  25394  ressatans  25529  lgamcvg2  25649  lgam1  25658  gam1  25659  efnnfsumcl  25697  efchtdvds  25753  ppiub  25797  lgslem2  25891  lgsfcl2  25896  lgsne0  25928  2lgslem1b  25985  padicabvf  26224  istrkg3ld  26264  axlowdimlem16  26760  upgrbi  26895  umgrbi  26903  lfuhgr1v0e  27053  cusgr0  27225  wlk2v2elem2  27950  upgr4cycl4dv4e  27979  konigsberglem4  28049  frgr0  28059  ex-pss  28222  ex-fl  28241  ex-mod  28243  isgrpoi  28290  grporn  28313  isabloi  28343  smcnlem  28489  lnocoi  28549  cncph  28611  cnbn  28661  cnchl  28708  norm3adifii  28940  hhph  28970  hhhl  28996  hlim0  29027  hlimf  29029  helch  29035  hsn0elch  29040  hhssabloilem  29053  hhssnv  29056  hhshsslem2  29060  hhssbnOLD  29071  shscli  29109  shintcli  29121  chintcli  29123  shsval2i  29179  pjhthlem2  29184  lejdii  29330  nonbooli  29443  pjrni  29494  pjfoi  29495  pjfi  29496  pjmf1  29508  df0op2  29544  idunop  29770  0cnop  29771  0cnfn  29772  idcnop  29773  idhmop  29774  0hmop  29775  0lnfn  29777  0bdop  29785  lnophsi  29793  lnopcoi  29795  lnopunii  29804  lnophmi  29810  nmcopex  29821  nmcoplb  29822  nmcfnex  29845  nmcfnlb  29846  imaelshi  29850  nlelshi  29852  nlelchi  29853  riesz4i  29855  riesz4  29856  riesz1  29857  cnlnadjlem6  29864  cnlnadjlem9  29867  cnlnadjeui  29869  cnlnadjeu  29870  nmopadji  29882  bdophsi  29888  bdopcoi  29890  nmopcoadji  29893  pjhmopi  29938  pjbdlni  29941  hmopidmchi  29943  mdslj1i  30111  rinvf1o  30394  nnindf  30556  rpdp2cl  30579  dp2ltc  30584  dpmul4  30611  s3clhash  30645  xrstos  30708  xrsclat  30709  xrge0tsmsd  30734  xrge0omnd  30754  reofld  30956  nn0archi  30959  ccfldextrr  31106  ccfldsrarelvec  31124  ccfldextdgrr  31125  xrge0iifmhm  31267  xrge0pluscn  31268  cnzh  31296  rezh  31297  qqhval2lem  31307  esum0  31393  esumcst  31407  esumpcvgval  31422  esumcvg  31430  dmvlsiga  31473  measdivcstALTV  31569  eulerpartlemt  31714  coinfliprv  31825  ballotlem2  31831  signswmnd  31912  logdivsqrle  32006  hgt750lem  32007  bnj906  32287  indispconn  32566  cnllysconn  32577  rellysconn  32583  msrf  32874  soseq  33181  bdayfo  33267  scutf  33358  brbigcup  33444  fobigcup  33446  brsingle  33463  fnsingle  33465  brimage  33472  funimage  33474  fnimage  33475  imageval  33476  brcart  33478  brapply  33484  brcup  33485  brcap  33486  funpartfun  33489  brub  33500  onsucconni  33870  onsucsuccmpi  33876  dnicn  33916  bj-wnfnf  34155  bj-nnfv  34170  bj-nnfa1  34175  bj-nnfe1  34176  bj-dtru  34226  bj-rabtr  34344  taupilem2  34708  taupi  34709  f1omptsnlem  34725  icoreresf  34741  relowlpssretop  34753  finxpreclem3  34782  matunitlindf  35027  mblfinlem2  35067  areacirc  35122  0totbnd  35183  heiborlem6  35226  refrelid  35893  idsymrel  35929  refrelsredund4  35999  refrelredund4  36002  disjALTV0  36116  disjALTVid  36117  isolatiN  36484  isomliN  36507  ishlatiN  36623  sn-dtru  39366  mzpclall  39612  jm2.20nn  39882  dfacbasgrp  39996  dgraaf  40035  ifpim3  40148  ifpim4  40150  ifpbi1b  40155  eu0  40172  iso0  40959  dvsid  40983  halffl  41881  resincncf  42470  0cnf  42472  iblempty  42560  dirkeritg  42697  fourierdlem62  42763  fourierdlem76  42777  fourierdlem103  42804  etransclem18  42847  etransclem46  42875  abnotbtaxb  43461  sprsymrelf1  43966  fmtnof1  44005  fmtno4prm  44045  prmdvdsfmtnof1  44057  31prm  44067  requad01  44092  0evenALTV  44159  1oddALTV  44161  2evenALTV  44163  6even  44182  8even  44184  6gbe  44242  7gbow  44243  8gbe  44244  9gbo  44245  11gbo  44246  uspgrsprf1  44328  1odd  44384  nnsgrp  44390  0even  44508  2even  44510  2zrngamgm  44516  2zrngasgrp  44517  2zrngamnd  44518  2zrngagrp  44520  2zrngmsgrp  44524  zlmodzxzldeplem3  44864  lvecpsslmod  44869  ldepsnlinc  44870  blennngt2o2  44959  blennn0e2  44961  ackval42  45063  rrx2xpref1o  45085  rrx2plordisom  45090  setrec2lem2  45177  aacllem  45282
  Copyright terms: Public domain W3C validator