Theorem mpbir2an 724

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3pm3.2i  1358  euequ  2625  eqssi  3929  elini  4099  dtruALT2  5336  exexneq  5407  opnzi  5447  so0  5601  we0  5650  difxp  6167  ord0  6435  dfiota4  6550  funi  6592  funcnvsn  6612  idfn  6689  fn0  6692  f0  6785  fconst  6790  f10  6881  f1o0  6885  f1oiOLD  6887  f1osn  6889  isoid  7360  porpss  7767  epweon  7813  epweonALT  7814  ordon  7815  omssnlim  7916  peano1  7924  fo1st  8045  fo2nd  8046  soseq  8203  iordsmo  8393  tfrlem7  8419  tfr1  8433  frfnom  8471  seqomlem2  8489  oawordeulem  8590  1onn  8677  2onn  8679  naddf  8719  mapsnf1o2  8950  canth2  9177  1sdom2  9267  unfilem2  9326  cantnfvalf  9693  cnfcom3clem  9733  ssttrcl  9743  tc2  9768  r111  9809  rankf  9829  setrec2lem2  10003  cardf2  10051  harcard  10086  r0weon  10118  infxpenc  10124  infxpenc2lem1  10125  alephon  10175  alephf1  10191  alephiso  10204  alephsmo  10208  alephf1ALT  10209  alephfplem4  10213  ackbij1lem17  10340  ackbij1  10342  ackbij2  10347  fin1a2lem2  10506  fin1a2lem4  10508  axcc2lem  10541  iunfo  10650  smobeth  10698  0tsk  10867  1pi  10995  nqerf  11042  axaddf  11257  axmulf  11258  axicn  11262  mpoaddf  11321  mpomulf  11322  mulnzcnf  11989  negiso  12324  dfnn2  12375  nnind  12380  0z  12731  dfuzi  12817  cnref1o  13140  elrpii  13150  0e0icopnf  13616  0e0iccpnf  13617  fldiv4p1lem1div2  14002  om2uzf1oi  14123  om2uzisoi  14124  uzrdgfni  14128  expcl2lem  14243  expclzlem  14253  expge0  14268  expge1  14269  faclbnd4lem1  14464  hashkf  14503  wwlktovf1  15139  sgnfo  15281  sqrtf  15560  fclim  15749  fprodn0f  16187  eff2  16296  reeff1  16317  ef01bndlem  16381  sin01bnd  16382  cos01bnd  16383  sin01gt0  16387  egt2lt3  16403  qnnen  16410  ruc  16440  halfleoddlt  16561  divalglem2  16594  divalglem9  16600  bitsf1  16645  sadaddlem  16665  2prm  16896  3prm  16898  1arith  17134  prmlem1a  17313  setsnid  17415  xpsff1o  17768  dmaf  18253  cdaf  18254  coapm  18275  0pos  18524  isposi  18526  letsr  18796  ex-chn1  18840  ex-chn2  18841  sgrp0b  18946  frmdplusg  19079  efmndsgrp  19111  smndex1sgrp  19136  smndex1mnd  19138  symg2bas  19637  pmtrsn  19763  odf  19781  efgsfo  19983  efgrelexlemb  19994  isabli  20040  rngmgpf  20409  mgpf  20505  prdscrngd  20581  xrsmgmdifsgrp  21745  cnmgpid  21765  xrs1cmn  21778  xrge0omnd  21781  zringnzr  21796  zringunit  21802  zringlpir  21803  zringndrg  21804  pzriprnglem5  21821  pzriprnglem7  21823  pzriprnglem9  21825  pzriprnglem13  21829  zzngim  21888  cnmsgngrp  21915  psgninv  21918  zrhpsgnmhm  21920  retos  21954  refld  21955  rzgrp  21959  pjpm  22044  matunitlindf  23026  fntopon  23272  istpsi  23290  cmpfi  23756  indisconn  23766  kqf  24096  fbssfi  24186  zfbas  24245  ptcmplem2  24402  prdstmdd  24473  tsmsfbas  24477  ismeti  24674  prdsxmslem2  24878  cnfldms  25124  cnnrg  25129  tgqioo  25149  xrtgioo  25156  recld2  25164  xrge0gsumle  25183  xrge0tsms  25184  addcnlem  25214  divcn  25219  abscncf  25252  recncf  25253  imcncf  25254  cjcncf  25255  icopnfhmeo  25294  xrhmeo  25297  cnllycmp  25307  isclmi0  25449  iscvsi  25480  cnstrcvs  25492  cncms  25706  ovolf  25833  ovolre  25876  opnmblALT  25954  dveflem  26329  mdegxrf  26416  iaaOLD  26682  ulmdm  26750  dvradcnv  26778  reeff1o  26804  reefiso  26805  reefgim  26807  recosf1o  26893  efifo  26905  logcn  27005  cxpcn3  27106  resqrtcn  27107  logb1  27127  logbmpt  27146  2logb9irrALT  27156  sqrt2cxp2logb9e3  27157  ressatans  27292  lgamcvg2  27412  lgam1  27421  gam1  27422  efnnfsumcl  27460  efchtdvds  27516  ppiub  27561  lgslem2  27655  lgsfcl2  27660  lgsne0  27692  2lgslem1b  27749  padicabvf  27988  bdayfo  28064  cutsf  28208  madef  28252  cutsfo  28321  addsf  28398  addsfo  28399  negsf  28468  negsfo  28469  negsf1o  28470  subsfo  28481  0ons  28672  1ons  28673  oniso  28687  dfn0s2  28748  1nns  28765  bdayn0sf1o  28786  zsoring  28825  twocut  28839  0reno  28912  1reno  28913  istrkg3ld  28953  axlowdimlem16  29565  upgrbi  29701  umgrbi  29709  lfuhgr1v0e  29865  cusgr0  30037  wlk2v2elem2  30787  upgr4cycl4dv4e  30816  konigsberglem4  30886  frgr0  30896  ex-pss  31059  ex-fl  31078  ex-mod  31080  isgrpoi  31130  grporn  31153  isabloi  31183  smcnlem  31329  lnocoi  31389  cncph  31451  cnbn  31501  cnchl  31548  norm3adifii  31780  hhph  31810  hhhl  31836  hlim0  31867  hlimf  31869  helch  31875  hsn0elch  31880  hhssabloilem  31893  hhssnv  31896  hhshsslem2  31900  hhssbnOLD  31911  shscli  31949  shintcli  31961  chintcli  31963  shsval2i  32019  pjhthlem2  32024  lejdii  32170  nonbooli  32283  pjrni  32334  pjfoi  32335  pjfi  32336  pjmf1  32348  df0op2  32384  idunop  32610  0cnop  32611  0cnfn  32612  idcnop  32613  idhmop  32614  0hmop  32615  0lnfn  32617  0bdop  32625  lnophsi  32633  lnopcoi  32635  lnopunii  32644  lnophmi  32650  nmcopex  32661  nmcoplb  32662  nmcfnex  32685  nmcfnlb  32686  imaelshi  32690  nlelshi  32692  nlelchi  32693  riesz4i  32695  riesz4  32696  riesz1  32697  cnlnadjlem6  32704  cnlnadjlem9  32707  cnlnadjeui  32709  cnlnadjeu  32710  nmopadji  32722  bdophsi  32728  bdopcoi  32730  nmopcoadji  32733  pjhmopi  32778  pjbdlni  32781  hmopidmchi  32783  mdslj1i  32951  rinvf1o  33296  nnindf  33481  rpdp2cl  33518  dp2ltc  33523  dpmul4  33550  s3clhash  33582  xrstos  33641  xrsclat  33642  xrge0tsmsd  33704  qfld  33929  cnfldfld  33973  reofld  33974  nn0archi  33978  zringidom  34153  zringfrac  34156  ccfldextrr  34348  ccfldsrarelvec  34373  ccfldextdgrr  34374  2sqr3minply  34482  xrge0iifmhm  34641  xrge0pluscn  34642  cnzh  34670  rezh  34671  qqhval2lem  34683  esum0  34751  esumcst  34765  esumpcvgval  34780  esumcvg  34788  dmvlsiga  34831  measdivcstALTV  34928  eulerpartlemt  35073  coinfliprv  35185  ballotlem2  35191  signswmnd  35256  logdivsqrle  35349  hgt750lem  35350  bnj906  35630  suceldifsn0  35791  xoromon  35794  rankfo  35817  fineqvnttrclse  35892  jf1  36010  jf1o  36011  indispconn  36166  cnllysconn  36177  rellysconn  36183  msrf  36474  onprcr  36631  brbigcup  36838  fobigcup  36840  brsingle  36857  fnsingle  36859  brimage  36866  funimage  36868  fnimage  36869  imageval  36870  brcart  36872  brapply  36878  brcup  36879  brcap  36880  funpartfun  36885  brub  36896  mpomulnzcnf  37266  onsucconni  37403  onsucsuccmpi  37409  dnicn  37536  bj-nnfv  37848  bj-wnfnf  37863  bj-nnfa1  37864  bj-nnfe1  37865  bj-rabtr  38021  bj-axreprepsep  38182  taupilem2  38435  taupi  38436  f1omptsnlem  38451  icoreresf  38467  relowlpssretop  38479  finxpreclem3  38508  mblfinlem2  38768  areacirc  38823  0totbnd  38899  heiborlem6  38942  dfsucmap3  39587  refrelid  39726  idsymrel  39769  trrelressn  39791  refrelsredund4  39840  refrelredund4  39843  disjALTV0  39978  disjALTVid  39979  antisymrelressn  39991  isolatiN  40465  isomliN  40488  ishlatiN  40604  mzpclall  43931  jm2.20nn  44197  dfacbasgrp  44302  dgraaf  44341  onexoegt  44438  omnord1  44499  oege2  44501  oenord1  44510  cantnftermord  44514  cantnf2  44519  omabs2  44526  omcl2  44527  ifpim3  44689  ifpim4  44691  ifpbi1b  44696  eu0  44713  omiscard  44736  iso0  45483  dvsid  45507  rankrelp  46145  hashomiso  46210  hfstructwe  46234  halffl  46517  resincncf  47090  0cnf  47092  iblempty  47180  dirkeritg  47317  fourierdlem62  47383  fourierdlem76  47397  fourierdlem103  47424  etransclem18  47467  etransclem46  47495  sinnpoly  48146  abnotbtaxb  48190  dfaiota3  48367  ceilhalf1  48613  sprsymrelf1  48783  fmtnof1  48825  fmtno4prm  48865  prmdvdsfmtnof1  48877  31prm  48887  requad01  48924  0evenALTV  48991  1oddALTV  48993  2evenALTV  48995  6even  49014  8even  49016  6gbe  49074  7gbow  49075  8gbe  49076  9gbo  49077  11gbo  49078  usgrexmpl1lem  49324  usgrexmpl2lem  49329  usgrexmpl2trifr  49340  gpg5grlim  49396  gpg5grlic  49397  uspgrsprf1  49450  1odd  49473  nnsgrp  49479  0even  49539  2even  49541  2zrngamgm  49547  2zrngasgrp  49548  2zrngamnd  49549  2zrngagrp  49551  2zrngmsgrp  49555  zlmodzxzldeplem3  49819  lvecpsslmod  49824  ldepsnlinc  49825  blennngt2o2  49909  blennn0e2  49911  ackval42  50013  rrx2plordisom  50041  slotresfo  50218  sepfsepc  50247  basresposfo  50297  oppff1  50469  setcsnterm  50830  setc1onsubc  50945  aacllem  51219  veroquadmodzerod  51264  veroquadnolindfd  51265