Theorem mpbir2an 721

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  3pm3.2i  1352  euequ  2623  eqssi  3952  elini  4151  dtruALT2  5326  exexneq  5401  opnzi  5441  so0  5591  we0  5640  difxp  6146  ord0  6396  dfiota4  6509  funi  6549  funcnvsn  6567  idfn  6645  fn0  6648  f0  6741  fconst  6746  f10  6836  f1o0  6840  f1oiOLD  6842  f1osn  6844  isoid  7309  porpss  7706  epweon  7754  epweonALT  7755  ordon  7756  omssnlim  7857  peano1  7865  fo1st  7986  fo2nd  7987  soseq  8134  iordsmo  8323  tfrlem7  8349  tfr1  8363  frfnom  8401  seqomlem2  8417  oawordeulem  8518  1onn  8605  2onn  8607  naddf  8647  mapsnf1o2  8872  canth2  9098  1sdom2  9188  unfilem2  9246  cantnfvalf  9617  cnfcom3clem  9657  ssttrcl  9667  tc2  9692  r111  9730  rankf  9749  cardf2  9898  harcard  9933  r0weon  9965  infxpenc  9971  infxpenc2lem1  9972  alephon  10022  alephf1  10038  alephiso  10051  alephsmo  10055  alephf1ALT  10056  alephfplem4  10060  ackbij1lem17  10188  ackbij1  10190  ackbij2  10195  fin1a2lem2  10355  fin1a2lem4  10357  axcc2lem  10390  iunfo  10493  smobeth  10541  0tsk  10710  1pi  10838  nqerf  10885  axaddf  11100  axmulf  11101  axicn  11105  mpoaddf  11164  mpomulf  11165  mulnzcnf  11830  negiso  12169  dfnn2  12220  nnind  12225  0z  12576  dfuzi  12661  cnref1o  12983  elrpii  12993  0e0icopnf  13459  0e0iccpnf  13460  fldiv4p1lem1div2  13842  om2uzf1oi  13963  om2uzisoi  13964  uzrdgfni  13968  expcl2lem  14083  expclzlem  14093  expge0  14108  expge1  14109  faclbnd4lem1  14303  hashkf  14342  wwlktovf1  14967  sqrtf  15374  fclim  15563  fprodn0f  16004  eff2  16114  reeff1  16135  ef01bndlem  16199  sin01bnd  16200  cos01bnd  16201  sin01gt0  16205  egt2lt3  16221  qnnen  16228  ruc  16258  halfleoddlt  16379  divalglem2  16412  divalglem9  16418  bitsf1  16463  sadaddlem  16483  2prm  16709  3prm  16711  1arith  16946  prmlem1a  17125  setsnid  17227  xpsff1o  17580  dmaf  18065  cdaf  18066  coapm  18087  0pos  18336  isposi  18338  letsr  18608  ex-chn1  18652  ex-chn2  18653  sgrp0b  18745  frmdplusg  18871  efmndsgrp  18903  smndex1sgrp  18928  smndex1mnd  18930  symg2bas  19416  pmtrsn  19542  odf  19560  efgsfo  19762  efgrelexlemb  19773  isabli  19819  rngmgpf  20186  mgpf  20277  prdscrngd  20349  xrsmgmdifsgrp  21441  cnmgpid  21461  xrs1cmn  21474  xrge0omnd  21477  zringnzr  21492  zringunit  21498  zringlpir  21499  zringndrg  21500  pzriprnglem5  21517  pzriprnglem7  21519  pzriprnglem9  21521  pzriprnglem13  21525  zzngim  21584  cnmsgngrp  21611  psgninv  21614  zrhpsgnmhm  21616  retos  21650  refld  21651  rzgrp  21655  pjpm  21740  fntopon  22964  istpsi  22982  cmpfi  23448  indisconn  23458  kqf  23787  fbssfi  23877  zfbas  23936  ptcmplem2  24093  prdstmdd  24164  tsmsfbas  24168  ismeti  24365  prdsxmslem2  24569  cnfldms  24815  cnnrg  24820  tgqioo  24840  xrtgioo  24847  recld2  24855  xrge0gsumle  24874  xrge0tsms  24875  addcnlem  24905  divcn  24910  abscncf  24943  recncf  24944  imcncf  24945  cjcncf  24946  icopnfhmeo  24985  xrhmeo  24988  cnllycmp  24998  isclmi0  25140  iscvsi  25171  cnstrcvs  25183  cncms  25397  ovolf  25524  ovolre  25567  opnmblALT  25645  dveflem  26021  mdegxrf  26108  iaa  26366  ulmdm  26433  dvradcnv  26461  reeff1o  26487  reefiso  26488  reefgim  26490  recosf1o  26577  efifo  26589  logcn  26689  cxpcn3  26790  resqrtcn  26791  logb1  26811  logbmpt  26830  2logb9irrALT  26840  sqrt2cxp2logb9e3  26841  ressatans  26976  lgamcvg2  27096  lgam1  27105  gam1  27106  efnnfsumcl  27144  efchtdvds  27200  ppiub  27245  lgslem2  27339  lgsfcl2  27344  lgsne0  27376  2lgslem1b  27433  padicabvf  27672  bdayfo  27718  cutsf  27862  madef  27906  cutsfo  27975  addsf  28052  addsfo  28053  negsf  28122  negsfo  28123  negsf1o  28124  subsfo  28135  0ons  28326  1ons  28327  oniso  28341  dfn0s2  28402  1nns  28419  bdayn0sf1o  28440  zsoring  28479  twocut  28493  0reno  28566  1reno  28567  istrkg3ld  28607  axlowdimlem16  29104  upgrbi  29240  umgrbi  29248  lfuhgr1v0e  29401  cusgr0  29573  wlk2v2elem2  30304  upgr4cycl4dv4e  30333  konigsberglem4  30403  frgr0  30413  ex-pss  30576  ex-fl  30595  ex-mod  30597  isgrpoi  30647  grporn  30670  isabloi  30700  smcnlem  30846  lnocoi  30906  cncph  30968  cnbn  31018  cnchl  31065  norm3adifii  31297  hhph  31327  hhhl  31353  hlim0  31384  hlimf  31386  helch  31392  hsn0elch  31397  hhssabloilem  31410  hhssnv  31413  hhshsslem2  31417  hhssbnOLD  31428  shscli  31466  shintcli  31478  chintcli  31480  shsval2i  31536  pjhthlem2  31541  lejdii  31687  nonbooli  31800  pjrni  31851  pjfoi  31852  pjfi  31853  pjmf1  31865  df0op2  31901  idunop  32127  0cnop  32128  0cnfn  32129  idcnop  32130  idhmop  32131  0hmop  32132  0lnfn  32134  0bdop  32142  lnophsi  32150  lnopcoi  32152  lnopunii  32161  lnophmi  32167  nmcopex  32178  nmcoplb  32179  nmcfnex  32202  nmcfnlb  32203  imaelshi  32207  nlelshi  32209  nlelchi  32210  riesz4i  32212  riesz4  32213  riesz1  32214  cnlnadjlem6  32221  cnlnadjlem9  32224  cnlnadjeui  32226  cnlnadjeu  32227  nmopadji  32239  bdophsi  32245  bdopcoi  32247  nmopcoadji  32250  pjhmopi  32295  pjbdlni  32298  hmopidmchi  32300  mdslj1i  32468  rinvf1o  32782  nnindf  32972  rpdp2cl  33020  dp2ltc  33025  dpmul4  33052  s3clhash  33087  xrstos  33149  xrsclat  33150  xrge0tsmsd  33214  qfld  33445  cnfldfld  33489  reofld  33490  nn0archi  33494  zringidom  33708  zringfrac  33711  ccfldextrr  33904  ccfldsrarelvec  33929  ccfldextdgrr  33930  2sqr3minply  34038  xrge0iifmhm  34197  xrge0pluscn  34198  cnzh  34226  rezh  34227  qqhval2lem  34239  esum0  34307  esumcst  34321  esumpcvgval  34336  esumcvg  34344  dmvlsiga  34387  measdivcstALTV  34483  eulerpartlemt  34629  coinfliprv  34741  ballotlem2  34747  signswmnd  34815  logdivsqrle  34908  hgt750lem  34909  bnj906  35189  xoromon  35348  fineqvnttrclse  35384  indispconn  35548  cnllysconn  35559  rellysconn  35565  msrf  35856  brbigcup  36210  fobigcup  36212  brsingle  36229  fnsingle  36231  brimage  36238  funimage  36240  fnimage  36241  imageval  36242  brcart  36244  brapply  36250  brcup  36251  brcap  36252  funpartfun  36257  brub  36268  mpomulnzcnf  36623  onsucconni  36761  onsucsuccmpi  36767  dnicn  36894  bj-nnfv  37207  bj-wnfnf  37222  bj-nnfa1  37223  bj-nnfe1  37224  bj-rabtr  37379  bj-axreprepsep  37524  taupilem2  37778  taupi  37779  f1omptsnlem  37794  icoreresf  37810  relowlpssretop  37822  finxpreclem3  37851  matunitlindf  38081  mblfinlem2  38121  areacirc  38176  0totbnd  38236  heiborlem6  38279  dfsucmap3  38926  refrelid  39065  idsymrel  39108  trrelressn  39130  refrelsredund4  39179  refrelredund4  39182  disjALTV0  39317  disjALTVid  39318  antisymrelressn  39330  isolatiN  39804  isomliN  39827  ishlatiN  39943  mzpclall  43272  jm2.20nn  43538  dfacbasgrp  43649  dgraaf  43688  onexoegt  43785  omnord1  43846  oege2  43848  oenord1  43857  cantnftermord  43861  cantnf2  43866  omabs2  43873  omcl2  43874  ifpim3  44036  ifpim4  44038  ifpbi1b  44043  eu0  44060  omiscard  44083  iso0  44847  dvsid  44871  rankrelp  45500  halffl  45839  resincncf  46413  0cnf  46415  iblempty  46503  dirkeritg  46640  fourierdlem62  46706  fourierdlem76  46720  fourierdlem103  46747  etransclem18  46790  etransclem46  46818  abnotbtaxb  47473  dfaiota3  47650  ceilhalf1  47896  sprsymrelf1  48066  fmtnof1  48108  fmtno4prm  48148  prmdvdsfmtnof1  48160  31prm  48170  requad01  48207  0evenALTV  48274  1oddALTV  48276  2evenALTV  48278  6even  48297  8even  48299  6gbe  48357  7gbow  48358  8gbe  48359  9gbo  48360  11gbo  48361  usgrexmpl1lem  48607  usgrexmpl2lem  48612  usgrexmpl2trifr  48623  gpg5grlim  48679  gpg5grlic  48680  uspgrsprf1  48733  1odd  48757  nnsgrp  48763  0even  48823  2even  48825  2zrngamgm  48831  2zrngasgrp  48832  2zrngamnd  48833  2zrngagrp  48835  2zrngmsgrp  48839  zlmodzxzldeplem3  49088  lvecpsslmod  49093  ldepsnlinc  49094  blennngt2o2  49178  blennn0e2  49180  ackval42  49282  rrx2xpref1o  49304  rrx2plordisom  49309  slotresfo  49484  sepfsepc  49513  basresposfo  49563  oppff1  49733  setcsnterm  50075  setc1onsubc  50187  setrec2lem2  50279  aacllem  50386