Theorem mpbir2an 711

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 709	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 231	1 ⊢ 𝜑

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3pm3.2i  1340  euequ  2597  eqssi  3950  elini  4151  dtruALT2  5315  exexneq  5384  opnzi  5422  so0  5570  we0  5619  difxp  6122  ord0  6371  dfiota4  6484  funi  6524  funcnvsn  6542  idfn  6620  fn0  6623  f0  6715  fconst  6720  f10  6807  f1o0  6811  f1oiOLD  6813  f1osn  6815  isoid  7275  porpss  7672  epweon  7720  epweonALT  7721  ordon  7722  omssnlim  7823  peano1  7831  fo1st  7953  fo2nd  7954  soseq  8101  iordsmo  8289  tfrlem7  8314  tfr1  8328  frfnom  8366  seqomlem2  8382  oawordeulem  8481  1onn  8568  2onn  8570  naddf  8609  mapsnf1o2  8832  canth2  9058  1sdom2  9148  unfilem2  9206  cantnfvalf  9574  cnfcom3clem  9614  ssttrcl  9624  tc2  9649  r111  9687  rankf  9706  cardf2  9855  harcard  9890  r0weon  9922  infxpenc  9928  infxpenc2lem1  9929  alephon  9979  alephf1  9995  alephiso  10008  alephsmo  10012  alephf1ALT  10013  alephfplem4  10017  ackbij1lem17  10145  ackbij1  10147  ackbij2  10152  fin1a2lem2  10311  fin1a2lem4  10313  axcc2lem  10346  iunfo  10449  smobeth  10497  0tsk  10666  1pi  10794  nqerf  10841  axaddf  11056  axmulf  11057  axicn  11061  mpoaddf  11120  mpomulf  11121  mulnzcnf  11783  negiso  12122  dfnn2  12158  nnind  12163  0z  12499  dfuzi  12583  cnref1o  12898  elrpii  12908  0e0icopnf  13374  0e0iccpnf  13375  fldiv4p1lem1div2  13755  om2uzf1oi  13876  om2uzisoi  13877  uzrdgfni  13881  expcl2lem  13996  expclzlem  14006  expge0  14021  expge1  14022  faclbnd4lem1  14216  hashkf  14255  wwlktovf1  14880  sqrtf  15287  fclim  15476  fprodn0f  15914  eff2  16024  reeff1  16045  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  sin01gt0  16115  egt2lt3  16131  qnnen  16138  ruc  16168  halfleoddlt  16289  divalglem2  16322  divalglem9  16328  bitsf1  16373  sadaddlem  16393  2prm  16619  3prm  16621  1arith  16855  prmlem1a  17034  setsnid  17135  xpsff1o  17488  dmaf  17973  cdaf  17974  coapm  17995  0pos  18244  isposi  18246  letsr  18516  ex-chn1  18560  ex-chn2  18561  sgrp0b  18653  frmdplusg  18779  efmndsgrp  18811  smndex1sgrp  18833  smndex1mnd  18835  symg2bas  19322  pmtrsn  19448  odf  19466  efgsfo  19668  efgrelexlemb  19679  isabli  19725  rngmgpf  20092  mgpf  20183  prdscrngd  20257  xrsmgmdifsgrp  21363  cnmgpid  21384  xrs1cmn  21397  xrge0omnd  21400  zringnzr  21415  zringunit  21421  zringlpir  21422  zringndrg  21423  pzriprnglem5  21440  pzriprnglem7  21442  pzriprnglem9  21444  pzriprnglem13  21448  zzngim  21507  cnmsgngrp  21534  psgninv  21537  zrhpsgnmhm  21539  retos  21573  refld  21574  rzgrp  21578  pjpm  21663  fntopon  22868  istpsi  22886  cmpfi  23352  indisconn  23362  kqf  23691  fbssfi  23781  zfbas  23840  ptcmplem2  23997  prdstmdd  24068  tsmsfbas  24072  ismeti  24269  prdsxmslem2  24473  cnfldms  24719  cnnrg  24724  tgqioo  24744  xrtgioo  24751  recld2  24759  xrge0gsumle  24778  xrge0tsms  24779  addcnlem  24809  divcnOLD  24813  divcn  24815  abscncf  24850  recncf  24851  imcncf  24852  cjcncf  24853  icopnfhmeo  24897  xrhmeo  24900  cnllycmp  24911  isclmi0  25054  iscvsi  25085  cnstrcvs  25097  cncms  25311  ovolf  25439  ovolre  25482  opnmblALT  25560  dveflem  25939  mdegxrf  26029  iaa  26289  ulmdm  26358  dvradcnv  26386  reeff1o  26413  reefiso  26414  reefgim  26416  recosf1o  26500  efifo  26512  logcn  26612  cxpcn3  26714  resqrtcn  26715  logb1  26735  logbmpt  26754  2logb9irrALT  26764  sqrt2cxp2logb9e3  26765  ressatans  26900  lgamcvg2  27021  lgam1  27030  gam1  27031  efnnfsumcl  27069  efchtdvds  27125  ppiub  27171  lgslem2  27265  lgsfcl2  27270  lgsne0  27302  2lgslem1b  27359  padicabvf  27598  bdayfo  27645  cutsf  27788  madef  27832  cutsfo  27901  addsf  27978  addsfo  27979  negsf  28048  negsfo  28049  negsf1o  28050  subsfo  28061  0ons  28252  1ons  28253  oniso  28267  dfn0s2  28328  1nns  28345  bdayn0sf1o  28366  zsoring  28405  twocut  28419  0reno  28492  1reno  28493  istrkg3ld  28533  axlowdimlem16  29030  upgrbi  29166  umgrbi  29174  lfuhgr1v0e  29327  cusgr0  29499  wlk2v2elem2  30231  upgr4cycl4dv4e  30260  konigsberglem4  30330  frgr0  30340  ex-pss  30503  ex-fl  30522  ex-mod  30524  isgrpoi  30573  grporn  30596  isabloi  30626  smcnlem  30772  lnocoi  30832  cncph  30894  cnbn  30944  cnchl  30991  norm3adifii  31223  hhph  31253  hhhl  31279  hlim0  31310  hlimf  31312  helch  31318  hsn0elch  31323  hhssabloilem  31336  hhssnv  31339  hhshsslem2  31343  hhssbnOLD  31354  shscli  31392  shintcli  31404  chintcli  31406  shsval2i  31462  pjhthlem2  31467  lejdii  31613  nonbooli  31726  pjrni  31777  pjfoi  31778  pjfi  31779  pjmf1  31791  df0op2  31827  idunop  32053  0cnop  32054  0cnfn  32055  idcnop  32056  idhmop  32057  0hmop  32058  0lnfn  32060  0bdop  32068  lnophsi  32076  lnopcoi  32078  lnopunii  32087  lnophmi  32093  nmcopex  32104  nmcoplb  32105  nmcfnex  32128  nmcfnlb  32129  imaelshi  32133  nlelshi  32135  nlelchi  32136  riesz4i  32138  riesz4  32139  riesz1  32140  cnlnadjlem6  32147  cnlnadjlem9  32150  cnlnadjeui  32152  cnlnadjeu  32153  nmopadji  32165  bdophsi  32171  bdopcoi  32173  nmopcoadji  32176  pjhmopi  32221  pjbdlni  32224  hmopidmchi  32226  mdslj1i  32394  rinvf1o  32708  nnindf  32900  rpdp2cl  32963  dp2ltc  32968  dpmul4  32995  s3clhash  33030  xrstos  33092  xrsclat  33093  xrge0tsmsd  33155  qfld  33379  cnfldfld  33423  reofld  33424  nn0archi  33428  zringidom  33632  zringfrac  33635  ccfldextrr  33803  ccfldsrarelvec  33828  ccfldextdgrr  33829  2sqr3minply  33937  xrge0iifmhm  34096  xrge0pluscn  34097  cnzh  34125  rezh  34126  qqhval2lem  34138  esum0  34206  esumcst  34220  esumpcvgval  34235  esumcvg  34243  dmvlsiga  34286  measdivcstALTV  34382  eulerpartlemt  34528  coinfliprv  34640  ballotlem2  34646  signswmnd  34714  logdivsqrle  34807  hgt750lem  34808  bnj906  35086  xoromon  35245  fineqvnttrclse  35280  indispconn  35428  cnllysconn  35439  rellysconn  35445  msrf  35736  brbigcup  36090  fobigcup  36092  brsingle  36109  fnsingle  36111  brimage  36118  funimage  36120  fnimage  36121  imageval  36122  brcart  36124  brapply  36130  brcup  36131  brcap  36132  funpartfun  36137  brub  36148  mpomulnzcnf  36493  onsucconni  36631  onsucsuccmpi  36637  dnicn  36692  bj-wnfnf  36940  bj-nnfv  36955  bj-nnfa1  36960  bj-nnfe1  36961  bj-rabtr  37131  taupilem2  37523  taupi  37524  f1omptsnlem  37537  icoreresf  37553  relowlpssretop  37565  finxpreclem3  37594  matunitlindf  37815  mblfinlem2  37855  areacirc  37910  0totbnd  37970  heiborlem6  38013  dfsucmap3  38633  refrelid  38771  idsymrel  38814  trrelressn  38836  refrelsredund4  38885  refrelredund4  38888  disjALTV0  39009  disjALTVid  39010  antisymrelressn  39019  isolatiN  39472  isomliN  39495  ishlatiN  39611  mzpclall  42965  jm2.20nn  43235  dfacbasgrp  43346  dgraaf  43385  onexoegt  43482  omnord1  43543  oege2  43545  oenord1  43554  cantnftermord  43558  cantnf2  43563  omabs2  43570  omcl2  43571  ifpim3  43733  ifpim4  43735  ifpbi1b  43740  eu0  43757  omiscard  43780  iso0  44544  dvsid  44568  rankrelp  45197  halffl  45540  resincncf  46115  0cnf  46117  iblempty  46205  dirkeritg  46342  fourierdlem62  46408  fourierdlem76  46422  fourierdlem103  46449  etransclem18  46492  etransclem46  46520  abnotbtaxb  47157  dfaiota3  47334  ceilhalf1  47576  sprsymrelf1  47738  fmtnof1  47777  fmtno4prm  47817  prmdvdsfmtnof1  47829  31prm  47839  requad01  47863  0evenALTV  47930  1oddALTV  47932  2evenALTV  47934  6even  47953  8even  47955  6gbe  48013  7gbow  48014  8gbe  48015  9gbo  48016  11gbo  48017  usgrexmpl1lem  48263  usgrexmpl2lem  48268  usgrexmpl2trifr  48279  gpg5grlim  48335  gpg5grlic  48336  uspgrsprf1  48389  1odd  48413  nnsgrp  48419  0even  48479  2even  48481  2zrngamgm  48487  2zrngasgrp  48488  2zrngamnd  48489  2zrngagrp  48491  2zrngmsgrp  48495  zlmodzxzldeplem3  48744  lvecpsslmod  48749  ldepsnlinc  48750  blennngt2o2  48834  blennn0e2  48836  ackval42  48938  rrx2xpref1o  48960  rrx2plordisom  48965  slotresfo  49140  sepfsepc  49169  basresposfo  49219  oppff1  49389  setcsnterm  49731  setc1onsubc  49843  setrec2lem2  49935  aacllem  50042