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  2592  eqssi  3951  elini  4149  dtruALT2  5308  exexneq  5377  opnzi  5414  so0  5562  we0  5611  difxp  6111  ord0  6360  dfiota4  6473  funi  6513  funcnvsn  6531  idfn  6609  fn0  6612  f0  6704  fconst  6709  f10  6796  f1o0  6800  f1oi  6801  f1osn  6803  isoid  7263  porpss  7660  epweon  7708  epweonALT  7709  ordon  7710  omssnlim  7811  peano1  7819  fo1st  7941  fo2nd  7942  soseq  8089  iordsmo  8277  tfrlem7  8302  tfr1  8316  frfnom  8354  seqomlem2  8370  oawordeulem  8469  1onn  8555  2onn  8557  naddf  8596  mapsnf1o2  8818  canth2  9043  1sdom2  9132  unfilem2  9190  cantnfvalf  9555  cnfcom3clem  9595  ssttrcl  9605  tc2  9632  r111  9665  rankf  9684  cardf2  9833  harcard  9868  r0weon  9900  infxpenc  9906  infxpenc2lem1  9907  alephon  9957  alephf1  9973  alephiso  9986  alephsmo  9990  alephf1ALT  9991  alephfplem4  9995  ackbij1lem17  10123  ackbij1  10125  ackbij2  10130  fin1a2lem2  10289  fin1a2lem4  10291  axcc2lem  10324  iunfo  10427  smobeth  10474  0tsk  10643  1pi  10771  nqerf  10818  axaddf  11033  axmulf  11034  axicn  11038  mpoaddf  11097  mpomulf  11098  mulnzcnf  11760  negiso  12099  dfnn2  12135  nnind  12140  0z  12476  dfuzi  12561  cnref1o  12880  elrpii  12890  0e0icopnf  13355  0e0iccpnf  13356  fldiv4p1lem1div2  13736  om2uzf1oi  13857  om2uzisoi  13858  uzrdgfni  13862  expcl2lem  13977  expclzlem  13987  expge0  14002  expge1  14003  faclbnd4lem1  14197  hashkf  14236  wwlktovf1  14861  sqrtf  15268  fclim  15457  fprodn0f  15895  eff2  16005  reeff1  16026  ef01bndlem  16090  sin01bnd  16091  cos01bnd  16092  sin01gt0  16096  egt2lt3  16112  qnnen  16119  ruc  16149  halfleoddlt  16270  divalglem2  16303  divalglem9  16309  bitsf1  16354  sadaddlem  16374  2prm  16600  3prm  16602  1arith  16836  prmlem1a  17015  setsnid  17116  xpsff1o  17468  dmaf  17953  cdaf  17954  coapm  17975  0pos  18224  isposi  18226  letsr  18496  ex-chn1  18540  ex-chn2  18541  sgrp0b  18633  frmdplusg  18759  efmndsgrp  18791  smndex1sgrp  18813  smndex1mnd  18815  symg2bas  19303  pmtrsn  19429  odf  19447  efgsfo  19649  efgrelexlemb  19660  isabli  19706  rngmgpf  20073  mgpf  20164  prdscrngd  20238  xrsmgmdifsgrp  21343  cnmgpid  21364  xrs1cmn  21377  xrge0omnd  21380  zringnzr  21395  zringunit  21401  zringlpir  21402  zringndrg  21403  pzriprnglem5  21420  pzriprnglem7  21422  pzriprnglem9  21424  pzriprnglem13  21428  zzngim  21487  cnmsgngrp  21514  psgninv  21517  zrhpsgnmhm  21519  retos  21553  refld  21554  rzgrp  21558  pjpm  21643  fntopon  22837  istpsi  22855  cmpfi  23321  indisconn  23331  kqf  23660  fbssfi  23750  zfbas  23809  ptcmplem2  23966  prdstmdd  24037  tsmsfbas  24041  ismeti  24238  prdsxmslem2  24442  cnfldms  24688  cnnrg  24693  tgqioo  24713  xrtgioo  24720  recld2  24728  xrge0gsumle  24747  xrge0tsms  24748  addcnlem  24778  divcnOLD  24782  divcn  24784  abscncf  24819  recncf  24820  imcncf  24821  cjcncf  24822  icopnfhmeo  24866  xrhmeo  24869  cnllycmp  24880  isclmi0  25023  iscvsi  25054  cnstrcvs  25066  cncms  25280  ovolf  25408  ovolre  25451  opnmblALT  25529  dveflem  25908  mdegxrf  25998  iaa  26258  ulmdm  26327  dvradcnv  26355  reeff1o  26382  reefiso  26383  reefgim  26385  recosf1o  26469  efifo  26481  logcn  26581  cxpcn3  26683  resqrtcn  26684  logb1  26704  logbmpt  26723  2logb9irrALT  26733  sqrt2cxp2logb9e3  26734  ressatans  26869  lgamcvg2  26990  lgam1  26999  gam1  27000  efnnfsumcl  27038  efchtdvds  27094  ppiub  27140  lgslem2  27234  lgsfcl2  27239  lgsne0  27271  2lgslem1b  27328  padicabvf  27567  bdayfo  27614  scutf  27751  madef  27795  scutfo  27848  addsf  27923  addsfo  27924  negsf  27992  negsfo  27993  negsf1o  27994  subsfo  28003  0ons  28191  1ons  28192  onsiso  28203  dfn0s2  28258  1nns  28275  bdayn0sf1o  28293  zsoring  28330  twocut  28344  0reno  28397  istrkg3ld  28437  axlowdimlem16  28933  upgrbi  29069  umgrbi  29077  lfuhgr1v0e  29230  cusgr0  29402  wlk2v2elem2  30131  upgr4cycl4dv4e  30160  konigsberglem4  30230  frgr0  30240  ex-pss  30403  ex-fl  30422  ex-mod  30424  isgrpoi  30473  grporn  30496  isabloi  30526  smcnlem  30672  lnocoi  30732  cncph  30794  cnbn  30844  cnchl  30891  norm3adifii  31123  hhph  31153  hhhl  31179  hlim0  31210  hlimf  31212  helch  31218  hsn0elch  31223  hhssabloilem  31236  hhssnv  31239  hhshsslem2  31243  hhssbnOLD  31254  shscli  31292  shintcli  31304  chintcli  31306  shsval2i  31362  pjhthlem2  31367  lejdii  31513  nonbooli  31626  pjrni  31677  pjfoi  31678  pjfi  31679  pjmf1  31691  df0op2  31727  idunop  31953  0cnop  31954  0cnfn  31955  idcnop  31956  idhmop  31957  0hmop  31958  0lnfn  31960  0bdop  31968  lnophsi  31976  lnopcoi  31978  lnopunii  31987  lnophmi  31993  nmcopex  32004  nmcoplb  32005  nmcfnex  32028  nmcfnlb  32029  imaelshi  32033  nlelshi  32035  nlelchi  32036  riesz4i  32038  riesz4  32039  riesz1  32040  cnlnadjlem6  32047  cnlnadjlem9  32050  cnlnadjeui  32052  cnlnadjeu  32053  nmopadji  32065  bdophsi  32071  bdopcoi  32073  nmopcoadji  32076  pjhmopi  32121  pjbdlni  32124  hmopidmchi  32126  mdslj1i  32294  rinvf1o  32607  nnindf  32797  rpdp2cl  32857  dp2ltc  32862  dpmul4  32889  s3clhash  32924  xrstos  32986  xrsclat  32987  xrge0tsmsd  33037  qfld  33258  cnfldfld  33302  reofld  33303  nn0archi  33307  zringidom  33511  zringfrac  33514  ccfldextrr  33654  ccfldsrarelvec  33679  ccfldextdgrr  33680  2sqr3minply  33788  xrge0iifmhm  33947  xrge0pluscn  33948  cnzh  33976  rezh  33977  qqhval2lem  33989  esum0  34057  esumcst  34071  esumpcvgval  34086  esumcvg  34094  dmvlsiga  34137  measdivcstALTV  34233  eulerpartlemt  34379  coinfliprv  34491  ballotlem2  34497  signswmnd  34565  logdivsqrle  34658  hgt750lem  34659  bnj906  34937  fineqvnttrclse  35132  indispconn  35266  cnllysconn  35277  rellysconn  35283  msrf  35574  brbigcup  35931  fobigcup  35933  brsingle  35950  fnsingle  35952  brimage  35959  funimage  35961  fnimage  35962  imageval  35963  brcart  35965  brapply  35971  brcup  35972  brcap  35973  funpartfun  35976  brub  35987  mpomulnzcnf  36332  onsucconni  36470  onsucsuccmpi  36476  dnicn  36525  bj-wnfnf  36772  bj-nnfv  36787  bj-nnfa1  36792  bj-nnfe1  36793  bj-rabtr  36963  taupilem2  37355  taupi  37356  f1omptsnlem  37369  icoreresf  37385  relowlpssretop  37397  finxpreclem3  37426  matunitlindf  37657  mblfinlem2  37697  areacirc  37752  0totbnd  37812  heiborlem6  37855  refrelid  38558  idsymrel  38597  trrelressn  38619  refrelsredund4  38668  refrelredund4  38671  disjALTV0  38791  disjALTVid  38792  antisymrelressn  38801  isolatiN  39254  isomliN  39277  ishlatiN  39393  mzpclall  42759  jm2.20nn  43029  dfacbasgrp  43140  dgraaf  43179  onexoegt  43276  omnord1  43337  oege2  43339  oenord1  43348  cantnftermord  43352  cantnf2  43357  omabs2  43364  omcl2  43365  ifpim3  43528  ifpim4  43530  ifpbi1b  43535  eu0  43552  omiscard  43575  iso0  44339  dvsid  44363  rankrelp  44992  halffl  45336  resincncf  45912  0cnf  45914  iblempty  46002  dirkeritg  46139  fourierdlem62  46205  fourierdlem76  46219  fourierdlem103  46246  etransclem18  46289  etransclem46  46317  abnotbtaxb  46945  dfaiota3  47122  ceilhalf1  47364  sprsymrelf1  47526  fmtnof1  47565  fmtno4prm  47605  prmdvdsfmtnof1  47617  31prm  47627  requad01  47651  0evenALTV  47718  1oddALTV  47720  2evenALTV  47722  6even  47741  8even  47743  6gbe  47801  7gbow  47802  8gbe  47803  9gbo  47804  11gbo  47805  usgrexmpl1lem  48051  usgrexmpl2lem  48056  usgrexmpl2trifr  48067  gpg5grlim  48123  gpg5grlic  48124  uspgrsprf1  48177  1odd  48201  nnsgrp  48207  0even  48267  2even  48269  2zrngamgm  48275  2zrngasgrp  48276  2zrngamnd  48277  2zrngagrp  48279  2zrngmsgrp  48283  zlmodzxzldeplem3  48533  lvecpsslmod  48538  ldepsnlinc  48539  blennngt2o2  48623  blennn0e2  48625  ackval42  48727  rrx2xpref1o  48749  rrx2plordisom  48754  slotresfo  48929  sepfsepc  48958  basresposfo  49008  oppff1  49179  setcsnterm  49521  setc1onsubc  49633  setrec2lem2  49725  aacllem  49832