Theorem mpbir2an 709

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

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 ⊢ 𝜒
2		mpbir2an.1	. . 3 ⊢ 𝜓
3		mpbir2an.maj	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
4	2, 3	mpbiran 707	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 233	1 ⊢ 𝜑

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3pm3.2i  1335  equsb1vOLDOLD  2517  sbtvOLD  2519  euequ  2683  eqssi  3985  elini  4172  dtru  5273  opnzi  5368  so0  5511  we0  5552  difxp  6023  ord0  6245  dfiota4  6349  funi  6389  funcnvsn  6406  idfn  6477  fnresiOLD  6479  fn0  6481  f0  6562  fconst  6567  f10  6649  f1o0  6653  f1oi  6654  f1osn  6656  isoid  7084  porpss  7455  epweon  7499  ordon  7500  omssnlim  7596  fo1st  7711  fo2nd  7712  wfrfun  7967  wfr1  7975  iordsmo  7996  tfrlem7  8021  tfr1  8035  frfnom  8072  seqomlem2  8089  oawordeulem  8182  mapsnf1o2  8460  canth2  8672  unfilem2  8785  cantnfvalf  9130  cnfcom3clem  9170  tc2  9186  r111  9206  rankf  9225  cardf2  9374  harcard  9409  r0weon  9440  infxpenc  9446  infxpenc2lem1  9447  alephon  9497  alephf1  9513  alephiso  9526  alephsmo  9530  alephf1ALT  9531  alephfplem4  9535  ackbij1lem17  9660  ackbij1  9662  ackbij2  9667  fin1a2lem2  9825  fin1a2lem4  9827  axcc2lem  9860  iunfo  9963  smobeth  10010  0tsk  10179  1pi  10307  nqerf  10354  axaddf  10569  axmulf  10570  axicn  10574  mulnzcnopr  11288  negiso  11623  dfnn2  11653  nnind  11658  0z  11995  dfuzi  12076  cnref1o  12387  elrpii  12395  0e0icopnf  12849  0e0iccpnf  12850  fz0to4untppr  13013  fldiv4p1lem1div2  13208  om2uzf1oi  13324  om2uzisoi  13325  uzrdgfni  13329  expcl2lem  13444  expclzlem  13456  expge0  13468  expge1  13469  faclbnd4lem1  13656  hashkf  13695  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  15748  divalglem9  15754  bitsf1  15797  sadaddlem  15817  2prm  16038  3prm  16040  1arith  16265  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  19311  prdscrngd  19365  xrsmgmdifsgrp  20584  xrs1cmn  20587  cnmgpid  20609  zringnzr  20631  zringunit  20637  zringlpir  20638  zringndrg  20639  zzngim  20701  cnmsgngrp  20725  psgninv  20728  zrhpsgnmhm  20730  retos  20764  refld  20765  rzgrp  20769  pjpm  20854  fntopon  21534  istpsi  21552  cmpfi  22018  indisconn  22028  kqf  22357  fbssfi  22447  zfbas  22506  ptcmplem2  22663  prdstmdd  22734  tsmsfbas  22738  ismeti  22937  prdsxmslem2  23141  cnfldms  23386  cnnrg  23391  tgqioo  23410  xrtgioo  23416  recld2  23424  xrge0gsumle  23443  xrge0tsms  23444  addcnlem  23474  divcn  23478  abscncf  23511  recncf  23512  imcncf  23513  cjcncf  23514  icopnfhmeo  23549  xrhmeo  23552  cnllycmp  23562  isclmi0  23704  iscvsi  23735  cnstrcvs  23747  cncms  23960  ovolf  24085  ovolre  24128  opnmblALT  24206  dveflem  24578  mdegxrf  24664  iaa  24916  ulmdm  24983  dvradcnv  25011  reeff1o  25037  reefiso  25038  reefgim  25040  recosf1o  25121  efifo  25133  logcn  25232  cxpcn3  25331  resqrtcn  25332  logb1  25349  logbmpt  25368  2logb9irrALT  25378  sqrt2cxp2logb9e3  25379  ressatans  25514  lgamcvg2  25634  lgam1  25643  gam1  25644  efnnfsumcl  25682  efchtdvds  25738  ppiub  25782  lgslem2  25876  lgsfcl2  25881  lgsne0  25913  2lgslem1b  25970  padicabvf  26209  istrkg3ld  26249  axlowdimlem16  26745  upgrbi  26880  umgrbi  26888  lfuhgr1v0e  27038  cusgr0  27210  wlk2v2elem2  27937  upgr4cycl4dv4e  27966  konigsberglem4  28036  frgr0  28046  ex-pss  28209  ex-fl  28228  ex-mod  28230  isgrpoi  28277  grporn  28300  isabloi  28330  smcnlem  28476  lnocoi  28536  cncph  28598  cnbn  28648  cnchl  28695  norm3adifii  28927  hhph  28957  hhhl  28983  hlim0  29014  hlimf  29016  helch  29022  hsn0elch  29027  hhssabloilem  29040  hhssnv  29043  hhshsslem2  29047  hhssbnOLD  29058  shscli  29096  shintcli  29108  chintcli  29110  shsval2i  29166  pjhthlem2  29171  lejdii  29317  nonbooli  29430  pjrni  29481  pjfoi  29482  pjfi  29483  pjmf1  29495  df0op2  29531  idunop  29757  0cnop  29758  0cnfn  29759  idcnop  29760  idhmop  29761  0hmop  29762  0lnfn  29764  0bdop  29772  lnophsi  29780  lnopcoi  29782  lnopunii  29791  lnophmi  29797  nmcopex  29808  nmcoplb  29809  nmcfnex  29832  nmcfnlb  29833  imaelshi  29837  nlelshi  29839  nlelchi  29840  riesz4i  29842  riesz4  29843  riesz1  29844  cnlnadjlem6  29851  cnlnadjlem9  29854  cnlnadjeui  29856  cnlnadjeu  29857  nmopadji  29869  bdophsi  29875  bdopcoi  29877  nmopcoadji  29880  pjhmopi  29925  pjbdlni  29928  hmopidmchi  29930  mdslj1i  30098  rinvf1o  30377  nnindf  30537  rpdp2cl  30560  dp2ltc  30565  dpmul4  30592  s3clhash  30626  xrstos  30668  xrsclat  30669  xrge0tsmsd  30694  xrge0omnd  30714  reofld  30915  nn0archi  30918  ccfldextrr  31040  ccfldsrarelvec  31058  ccfldextdgrr  31059  xrge0iifmhm  31184  xrge0pluscn  31185  cnzh  31213  rezh  31214  qqhval2lem  31224  esum0  31310  esumcst  31324  esumpcvgval  31339  esumcvg  31347  dmvlsiga  31390  measdivcstALTV  31486  eulerpartlemt  31631  coinfliprv  31742  ballotlem2  31748  signswmnd  31829  logdivsqrle  31923  hgt750lem  31924  bnj906  32204  indispconn  32483  cnllysconn  32494  rellysconn  32500  msrf  32791  soseq  33098  bdayfo  33184  scutf  33275  brbigcup  33361  fobigcup  33363  brsingle  33380  fnsingle  33382  brimage  33389  funimage  33391  fnimage  33392  imageval  33393  brcart  33395  brapply  33401  brcup  33402  brcap  33403  funpartfun  33406  brub  33417  onsucconni  33787  onsucsuccmpi  33793  dnicn  33833  bj-wnfnf  34070  bj-nnfv  34085  bj-nnfa1  34090  bj-nnfe1  34091  bj-dtru  34141  bj-rabtr  34250  taupilem2  34605  taupi  34606  f1omptsnlem  34619  icoreresf  34635  relowlpssretop  34647  finxpreclem3  34676  matunitlindf  34892  mblfinlem2  34932  areacirc  34989  0totbnd  35053  heiborlem6  35096  refrelid  35763  idsymrel  35799  refrelsredund4  35869  refrelredund4  35872  disjALTV0  35986  disjALTVid  35987  isolatiN  36354  isomliN  36377  ishlatiN  36493  sn-dtru  39118  mzpclall  39331  jm2.20nn  39601  dfacbasgrp  39715  dgraaf  39754  ifpim3  39869  ifpim4  39871  ifpbi1b  39876  eu0  39893  iso0  40646  dvsid  40670  halffl  41570  resincncf  42165  0cnf  42167  iblempty  42257  dirkeritg  42394  fourierdlem62  42460  fourierdlem76  42474  fourierdlem103  42501  etransclem18  42544  etransclem46  42572  abnotbtaxb  43158  sprsymrelf1  43665  fmtnof1  43704  fmtno4prm  43744  prmdvdsfmtnof1  43756  31prm  43767  requad01  43793  0evenALTV  43860  1oddALTV  43862  2evenALTV  43864  6even  43883  8even  43885  6gbe  43943  7gbow  43944  8gbe  43945  9gbo  43946  11gbo  43947  uspgrsprf1  44029  1odd  44085  nnsgrp  44091  0even  44209  2even  44211  2zrngamgm  44217  2zrngasgrp  44218  2zrngamnd  44219  2zrngagrp  44221  2zrngmsgrp  44225  zlmodzxzldeplem3  44564  lvecpsslmod  44569  ldepsnlinc  44570  blennngt2o2  44659  blennn0e2  44661  rrx2xpref1o  44712  rrx2plordisom  44717  setrec2lem2  44804  aacllem  44909