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  2591  eqssi  3966  elini  4165  dtruALT2  5328  exexneq  5397  dtruOLD  5404  opnzi  5437  so0  5587  we0  5636  difxp  6140  ord0  6389  dfiota4  6506  funi  6551  funcnvsn  6569  idfn  6649  fn0  6652  f0  6744  fconst  6749  f10  6836  f1o0  6840  f1oi  6841  f1osn  6843  isoid  7307  porpss  7706  epweon  7754  epweonALT  7755  ordon  7756  omssnlim  7860  peano1  7868  fo1st  7991  fo2nd  7992  soseq  8141  iordsmo  8329  tfrlem7  8354  tfr1  8368  frfnom  8406  seqomlem2  8422  oawordeulem  8521  1onn  8607  2onn  8609  naddf  8648  mapsnf1o2  8870  canth2  9100  1sdom2  9194  unfilem2  9262  cantnfvalf  9625  cnfcom3clem  9665  ssttrcl  9675  tc2  9702  r111  9735  rankf  9754  cardf2  9903  harcard  9938  r0weon  9972  infxpenc  9978  infxpenc2lem1  9979  alephon  10029  alephf1  10045  alephiso  10058  alephsmo  10062  alephf1ALT  10063  alephfplem4  10067  ackbij1lem17  10195  ackbij1  10197  ackbij2  10202  fin1a2lem2  10361  fin1a2lem4  10363  axcc2lem  10396  iunfo  10499  smobeth  10546  0tsk  10715  1pi  10843  nqerf  10890  axaddf  11105  axmulf  11106  axicn  11110  mpoaddf  11169  mpomulf  11170  mulnzcnf  11831  negiso  12170  dfnn2  12206  nnind  12211  0z  12547  dfuzi  12632  cnref1o  12951  elrpii  12961  0e0icopnf  13426  0e0iccpnf  13427  fldiv4p1lem1div2  13804  om2uzf1oi  13925  om2uzisoi  13926  uzrdgfni  13930  expcl2lem  14045  expclzlem  14055  expge0  14070  expge1  14071  faclbnd4lem1  14265  hashkf  14304  wwlktovf1  14930  sqrtf  15337  fclim  15526  fprodn0f  15964  eff2  16074  reeff1  16095  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  egt2lt3  16181  qnnen  16188  ruc  16218  halfleoddlt  16339  divalglem2  16372  divalglem9  16378  bitsf1  16423  sadaddlem  16443  2prm  16669  3prm  16671  1arith  16905  prmlem1a  17084  setsnid  17185  xpsff1o  17537  dmaf  18018  cdaf  18019  coapm  18040  0pos  18289  isposi  18291  letsr  18559  sgrp0b  18662  frmdplusg  18788  efmndsgrp  18820  smndex1sgrp  18842  smndex1mnd  18844  symg2bas  19330  pmtrsn  19456  odf  19474  efgsfo  19676  efgrelexlemb  19687  isabli  19733  rngmgpf  20073  mgpf  20164  prdscrngd  20238  xrsmgmdifsgrp  21327  xrs1cmn  21330  cnmgpid  21353  zringnzr  21377  zringunit  21383  zringlpir  21384  zringndrg  21385  pzriprnglem5  21402  pzriprnglem7  21404  pzriprnglem9  21406  pzriprnglem13  21410  zzngim  21469  cnmsgngrp  21495  psgninv  21498  zrhpsgnmhm  21500  retos  21534  refld  21535  rzgrp  21539  pjpm  21624  fntopon  22818  istpsi  22836  cmpfi  23302  indisconn  23312  kqf  23641  fbssfi  23731  zfbas  23790  ptcmplem2  23947  prdstmdd  24018  tsmsfbas  24022  ismeti  24220  prdsxmslem2  24424  cnfldms  24670  cnnrg  24675  tgqioo  24695  xrtgioo  24702  recld2  24710  xrge0gsumle  24729  xrge0tsms  24730  addcnlem  24760  divcnOLD  24764  divcn  24766  abscncf  24801  recncf  24802  imcncf  24803  cjcncf  24804  icopnfhmeo  24848  xrhmeo  24851  cnllycmp  24862  isclmi0  25005  iscvsi  25036  cnstrcvs  25048  cncms  25262  ovolf  25390  ovolre  25433  opnmblALT  25511  dveflem  25890  mdegxrf  25980  iaa  26240  ulmdm  26309  dvradcnv  26337  reeff1o  26364  reefiso  26365  reefgim  26367  recosf1o  26451  efifo  26463  logcn  26563  cxpcn3  26665  resqrtcn  26666  logb1  26686  logbmpt  26705  2logb9irrALT  26715  sqrt2cxp2logb9e3  26716  ressatans  26851  lgamcvg2  26972  lgam1  26981  gam1  26982  efnnfsumcl  27020  efchtdvds  27076  ppiub  27122  lgslem2  27216  lgsfcl2  27221  lgsne0  27253  2lgslem1b  27310  padicabvf  27549  bdayfo  27596  scutf  27731  madef  27771  scutfo  27823  addsf  27896  addsfo  27897  negsf  27965  negsfo  27966  negsf1o  27967  subsfo  27976  0ons  28164  1ons  28165  onsiso  28176  dfn0s2  28231  1nns  28248  bdayn0sf1o  28266  twocut  28316  0reno  28355  istrkg3ld  28395  axlowdimlem16  28891  upgrbi  29027  umgrbi  29035  lfuhgr1v0e  29188  cusgr0  29360  wlk2v2elem2  30092  upgr4cycl4dv4e  30121  konigsberglem4  30191  frgr0  30201  ex-pss  30364  ex-fl  30383  ex-mod  30385  isgrpoi  30434  grporn  30457  isabloi  30487  smcnlem  30633  lnocoi  30693  cncph  30755  cnbn  30805  cnchl  30852  norm3adifii  31084  hhph  31114  hhhl  31140  hlim0  31171  hlimf  31173  helch  31179  hsn0elch  31184  hhssabloilem  31197  hhssnv  31200  hhshsslem2  31204  hhssbnOLD  31215  shscli  31253  shintcli  31265  chintcli  31267  shsval2i  31323  pjhthlem2  31328  lejdii  31474  nonbooli  31587  pjrni  31638  pjfoi  31639  pjfi  31640  pjmf1  31652  df0op2  31688  idunop  31914  0cnop  31915  0cnfn  31916  idcnop  31917  idhmop  31918  0hmop  31919  0lnfn  31921  0bdop  31929  lnophsi  31937  lnopcoi  31939  lnopunii  31948  lnophmi  31954  nmcopex  31965  nmcoplb  31966  nmcfnex  31989  nmcfnlb  31990  imaelshi  31994  nlelshi  31996  nlelchi  31997  riesz4i  31999  riesz4  32000  riesz1  32001  cnlnadjlem6  32008  cnlnadjlem9  32011  cnlnadjeui  32013  cnlnadjeu  32014  nmopadji  32026  bdophsi  32032  bdopcoi  32034  nmopcoadji  32037  pjhmopi  32082  pjbdlni  32085  hmopidmchi  32087  mdslj1i  32255  rinvf1o  32561  nnindf  32751  rpdp2cl  32809  dp2ltc  32814  dpmul4  32841  s3clhash  32876  xrstos  32955  xrsclat  32956  xrge0tsmsd  33009  xrge0omnd  33032  qfld  33254  cnfldfld  33321  reofld  33322  nn0archi  33325  zringidom  33529  zringfrac  33532  ccfldextrr  33649  ccfldsrarelvec  33673  ccfldextdgrr  33674  2sqr3minply  33777  xrge0iifmhm  33936  xrge0pluscn  33937  cnzh  33965  rezh  33966  qqhval2lem  33978  esum0  34046  esumcst  34060  esumpcvgval  34075  esumcvg  34083  dmvlsiga  34126  measdivcstALTV  34222  eulerpartlemt  34369  coinfliprv  34481  ballotlem2  34487  signswmnd  34555  logdivsqrle  34648  hgt750lem  34649  bnj906  34927  indispconn  35228  cnllysconn  35239  rellysconn  35245  msrf  35536  brbigcup  35893  fobigcup  35895  brsingle  35912  fnsingle  35914  brimage  35921  funimage  35923  fnimage  35924  imageval  35925  brcart  35927  brapply  35933  brcup  35934  brcap  35935  funpartfun  35938  brub  35949  mpomulnzcnf  36294  onsucconni  36432  onsucsuccmpi  36438  dnicn  36487  bj-wnfnf  36734  bj-nnfv  36749  bj-nnfa1  36754  bj-nnfe1  36755  bj-rabtr  36925  taupilem2  37317  taupi  37318  f1omptsnlem  37331  icoreresf  37347  relowlpssretop  37359  finxpreclem3  37388  matunitlindf  37619  mblfinlem2  37659  areacirc  37714  0totbnd  37774  heiborlem6  37817  refrelid  38520  idsymrel  38559  trrelressn  38581  refrelsredund4  38630  refrelredund4  38633  disjALTV0  38753  disjALTVid  38754  antisymrelressn  38763  isolatiN  39216  isomliN  39239  ishlatiN  39355  mzpclall  42722  jm2.20nn  42993  dfacbasgrp  43104  dgraaf  43143  onexoegt  43240  omnord1  43301  oege2  43303  oenord1  43312  cantnftermord  43316  cantnf2  43321  omabs2  43328  omcl2  43329  ifpim3  43492  ifpim4  43494  ifpbi1b  43499  eu0  43516  omiscard  43539  iso0  44303  dvsid  44327  rankrelp  44957  halffl  45301  resincncf  45880  0cnf  45882  iblempty  45970  dirkeritg  46107  fourierdlem62  46173  fourierdlem76  46187  fourierdlem103  46214  etransclem18  46257  etransclem46  46285  abnotbtaxb  46920  dfaiota3  47097  ceilhalf1  47339  sprsymrelf1  47501  fmtnof1  47540  fmtno4prm  47580  prmdvdsfmtnof1  47592  31prm  47602  requad01  47626  0evenALTV  47693  1oddALTV  47695  2evenALTV  47697  6even  47716  8even  47718  6gbe  47776  7gbow  47777  8gbe  47778  9gbo  47779  11gbo  47780  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2trifr  48032  gpg5grlic  48088  uspgrsprf1  48139  1odd  48163  nnsgrp  48169  0even  48229  2even  48231  2zrngamgm  48237  2zrngasgrp  48238  2zrngamnd  48239  2zrngagrp  48241  2zrngmsgrp  48245  zlmodzxzldeplem3  48495  lvecpsslmod  48500  ldepsnlinc  48501  blennngt2o2  48585  blennn0e2  48587  ackval42  48689  rrx2xpref1o  48711  rrx2plordisom  48716  slotresfo  48891  sepfsepc  48920  basresposfo  48970  oppff1  49141  setcsnterm  49483  setc1onsubc  49595  setrec2lem2  49687  aacllem  49794