Theorem mpbir2an 723

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 401

This theorem is referenced by:  3pm3.2i  1358  euequ  2625  eqssi  3954  elini  4153  dtruALT2  5343  exexneq  5418  opnzi  5458  so0  5609  we0  5658  difxp  6163  ord0  6417  dfiota4  6530  funi  6570  funcnvsn  6588  idfn  6665  fn0  6668  f0  6761  fconst  6766  f10  6856  f1o0  6860  f1oiOLD  6862  f1osn  6864  isoid  7329  porpss  7726  epweon  7775  epweonALT  7776  ordon  7777  omssnlim  7878  peano1  7886  fo1st  8007  fo2nd  8008  soseq  8156  iordsmo  8345  tfrlem7  8371  tfr1  8385  frfnom  8423  seqomlem2  8439  oawordeulem  8540  1onn  8627  2onn  8629  naddf  8669  mapsnf1o2  8893  canth2  9119  1sdom2  9209  unfilem2  9267  cantnfvalf  9635  cnfcom3clem  9675  ssttrcl  9685  tc2  9710  r111  9748  rankf  9767  cardf2  9930  harcard  9965  r0weon  9997  infxpenc  10003  infxpenc2lem1  10004  alephon  10054  alephf1  10070  alephiso  10083  alephsmo  10087  alephf1ALT  10088  alephfplem4  10092  ackbij1lem17  10219  ackbij1  10221  ackbij2  10226  fin1a2lem2  10386  fin1a2lem4  10388  axcc2lem  10421  iunfo  10524  smobeth  10572  0tsk  10741  1pi  10869  nqerf  10916  axaddf  11131  axmulf  11132  axicn  11136  mpoaddf  11195  mpomulf  11196  mulnzcnf  11861  negiso  12196  dfnn2  12247  nnind  12252  0z  12603  dfuzi  12688  cnref1o  13010  elrpii  13020  0e0icopnf  13486  0e0iccpnf  13487  fldiv4p1lem1div2  13870  om2uzf1oi  13991  om2uzisoi  13992  uzrdgfni  13996  expcl2lem  14111  expclzlem  14121  expge0  14136  expge1  14137  faclbnd4lem1  14331  hashkf  14370  wwlktovf1  14996  sgnfo  15138  sqrtf  15417  fclim  15606  fprodn0f  16047  eff2  16156  reeff1  16177  ef01bndlem  16241  sin01bnd  16242  cos01bnd  16243  sin01gt0  16247  egt2lt3  16263  qnnen  16270  ruc  16300  halfleoddlt  16421  divalglem2  16454  divalglem9  16460  bitsf1  16505  sadaddlem  16525  2prm  16751  3prm  16753  1arith  16988  prmlem1a  17167  setsnid  17269  xpsff1o  17622  dmaf  18107  cdaf  18108  coapm  18129  0pos  18378  isposi  18380  letsr  18650  ex-chn1  18694  ex-chn2  18695  sgrp0b  18787  frmdplusg  18914  efmndsgrp  18946  smndex1sgrp  18971  smndex1mnd  18973  symg2bas  19464  pmtrsn  19590  odf  19608  efgsfo  19810  efgrelexlemb  19821  isabli  19867  rngmgpf  20236  mgpf  20331  prdscrngd  20404  xrsmgmdifsgrp  21540  cnmgpid  21560  xrs1cmn  21573  xrge0omnd  21576  zringnzr  21591  zringunit  21597  zringlpir  21598  zringndrg  21599  pzriprnglem5  21616  pzriprnglem7  21618  pzriprnglem9  21620  pzriprnglem13  21624  zzngim  21683  cnmsgngrp  21710  psgninv  21713  zrhpsgnmhm  21715  retos  21749  refld  21750  rzgrp  21754  pjpm  21839  fntopon  23062  istpsi  23080  cmpfi  23546  indisconn  23556  kqf  23885  fbssfi  23975  zfbas  24034  ptcmplem2  24191  prdstmdd  24262  tsmsfbas  24266  ismeti  24463  prdsxmslem2  24667  cnfldms  24913  cnnrg  24918  tgqioo  24938  xrtgioo  24945  recld2  24953  xrge0gsumle  24972  xrge0tsms  24973  addcnlem  25003  divcn  25008  abscncf  25041  recncf  25042  imcncf  25043  cjcncf  25044  icopnfhmeo  25083  xrhmeo  25086  cnllycmp  25096  isclmi0  25238  iscvsi  25269  cnstrcvs  25281  cncms  25495  ovolf  25622  ovolre  25665  opnmblALT  25743  dveflem  26119  mdegxrf  26206  iaa  26469  ulmdm  26537  dvradcnv  26565  reeff1o  26591  reefiso  26592  reefgim  26594  recosf1o  26681  efifo  26693  logcn  26793  cxpcn3  26894  resqrtcn  26895  logb1  26915  logbmpt  26934  2logb9irrALT  26944  sqrt2cxp2logb9e3  26945  ressatans  27080  lgamcvg2  27200  lgam1  27209  gam1  27210  efnnfsumcl  27248  efchtdvds  27304  ppiub  27349  lgslem2  27443  lgsfcl2  27448  lgsne0  27480  2lgslem1b  27537  padicabvf  27776  bdayfo  27822  cutsf  27966  madef  28010  cutsfo  28079  addsf  28156  addsfo  28157  negsf  28226  negsfo  28227  negsf1o  28228  subsfo  28239  0ons  28430  1ons  28431  oniso  28445  dfn0s2  28506  1nns  28523  bdayn0sf1o  28544  zsoring  28583  twocut  28597  0reno  28670  1reno  28671  istrkg3ld  28711  axlowdimlem16  29288  upgrbi  29424  umgrbi  29432  lfuhgr1v0e  29585  cusgr0  29757  wlk2v2elem2  30488  upgr4cycl4dv4e  30517  konigsberglem4  30587  frgr0  30597  ex-pss  30760  ex-fl  30779  ex-mod  30781  isgrpoi  30831  grporn  30854  isabloi  30884  smcnlem  31030  lnocoi  31090  cncph  31152  cnbn  31202  cnchl  31249  norm3adifii  31481  hhph  31511  hhhl  31537  hlim0  31568  hlimf  31570  helch  31576  hsn0elch  31581  hhssabloilem  31594  hhssnv  31597  hhshsslem2  31601  hhssbnOLD  31612  shscli  31650  shintcli  31662  chintcli  31664  shsval2i  31720  pjhthlem2  31725  lejdii  31871  nonbooli  31984  pjrni  32035  pjfoi  32036  pjfi  32037  pjmf1  32049  df0op2  32085  idunop  32311  0cnop  32312  0cnfn  32313  idcnop  32314  idhmop  32315  0hmop  32316  0lnfn  32318  0bdop  32326  lnophsi  32334  lnopcoi  32336  lnopunii  32345  lnophmi  32351  nmcopex  32362  nmcoplb  32363  nmcfnex  32386  nmcfnlb  32387  imaelshi  32391  nlelshi  32393  nlelchi  32394  riesz4i  32396  riesz4  32397  riesz1  32398  cnlnadjlem6  32405  cnlnadjlem9  32408  cnlnadjeui  32410  cnlnadjeu  32411  nmopadji  32423  bdophsi  32429  bdopcoi  32431  nmopcoadji  32434  pjhmopi  32479  pjbdlni  32482  hmopidmchi  32484  mdslj1i  32652  rinvf1o  32956  nnindf  33145  rpdp2cl  33182  dp2ltc  33187  dpmul4  33214  s3clhash  33249  xrstos  33311  xrsclat  33312  xrge0tsmsd  33374  qfld  33599  cnfldfld  33643  reofld  33644  nn0archi  33648  zringidom  33822  zringfrac  33825  ccfldextrr  34017  ccfldsrarelvec  34042  ccfldextdgrr  34043  2sqr3minply  34151  xrge0iifmhm  34310  xrge0pluscn  34311  cnzh  34339  rezh  34340  qqhval2lem  34352  esum0  34420  esumcst  34434  esumpcvgval  34449  esumcvg  34457  dmvlsiga  34500  measdivcstALTV  34596  eulerpartlemt  34742  coinfliprv  34854  ballotlem2  34860  signswmnd  34925  logdivsqrle  35018  hgt750lem  35019  bnj906  35299  xoromon  35460  rankfo  35486  fineqvnttrclse  35518  indispconn  35707  cnllysconn  35718  rellysconn  35724  msrf  36015  brbigcup  36369  fobigcup  36371  brsingle  36388  fnsingle  36390  brimage  36397  funimage  36399  fnimage  36400  imageval  36401  brcart  36403  brapply  36409  brcup  36410  brcap  36411  funpartfun  36416  brub  36427  mpomulnzcnf  36792  onsucconni  36929  onsucsuccmpi  36935  dnicn  37062  bj-nnfv  37374  bj-wnfnf  37389  bj-nnfa1  37390  bj-nnfe1  37391  bj-rabtr  37547  bj-axreprepsep  37693  taupilem2  37947  taupi  37948  f1omptsnlem  37963  icoreresf  37979  relowlpssretop  37991  finxpreclem3  38020  matunitlindf  38250  mblfinlem2  38290  areacirc  38345  0totbnd  38405  heiborlem6  38448  dfsucmap3  39093  refrelid  39232  idsymrel  39275  trrelressn  39297  refrelsredund4  39346  refrelredund4  39349  disjALTV0  39484  disjALTVid  39485  antisymrelressn  39497  isolatiN  39971  isomliN  39994  ishlatiN  40110  mzpclall  43441  jm2.20nn  43707  dfacbasgrp  43818  dgraaf  43857  onexoegt  43954  omnord1  44015  oege2  44017  oenord1  44026  cantnftermord  44030  cantnf2  44035  omabs2  44042  omcl2  44043  ifpim3  44205  ifpim4  44207  ifpbi1b  44212  eu0  44229  omiscard  44252  iso0  45000  dvsid  45024  rankrelp  45652  hashomiso  45717  halffl  45998  resincncf  46572  0cnf  46574  iblempty  46662  dirkeritg  46799  fourierdlem62  46865  fourierdlem76  46879  fourierdlem103  46906  etransclem18  46949  etransclem46  46977  abnotbtaxb  47635  dfaiota3  47812  ceilhalf1  48058  sprsymrelf1  48228  fmtnof1  48270  fmtno4prm  48310  prmdvdsfmtnof1  48322  31prm  48332  requad01  48369  0evenALTV  48436  1oddALTV  48438  2evenALTV  48440  6even  48459  8even  48461  6gbe  48519  7gbow  48520  8gbe  48521  9gbo  48522  11gbo  48523  usgrexmpl1lem  48769  usgrexmpl2lem  48774  usgrexmpl2trifr  48785  gpg5grlim  48841  gpg5grlic  48842  uspgrsprf1  48895  1odd  48919  nnsgrp  48925  0even  48985  2even  48987  2zrngamgm  48993  2zrngasgrp  48994  2zrngamnd  48995  2zrngagrp  48997  2zrngmsgrp  49001  zlmodzxzldeplem3  49265  lvecpsslmod  49270  ldepsnlinc  49271  blennngt2o2  49355  blennn0e2  49357  ackval42  49459  rrx2xpref1o  49481  rrx2plordisom  49486  slotresfo  49660  sepfsepc  49689  basresposfo  49739  oppff1  49909  setcsnterm  50251  setc1onsubc  50363  setrec2lem2  50455  aacllem  50584