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  2628  eqssi  3956  elini  4155  dtruALT2  5346  exexneq  5421  opnzi  5461  so0  5612  we0  5661  difxp  6166  ord0  6422  dfiota4  6535  funi  6575  funcnvsn  6593  idfn  6670  fn0  6673  f0  6766  fconst  6771  f10  6861  f1o0  6865  f1oiOLD  6867  f1osn  6869  isoid  7338  porpss  7737  epweon  7783  epweonALT  7784  ordon  7785  omssnlim  7886  peano1  7894  fo1st  8015  fo2nd  8016  soseq  8164  iordsmo  8353  tfrlem7  8379  tfr1  8393  frfnom  8431  seqomlem2  8447  oawordeulem  8548  1onn  8635  2onn  8637  naddf  8677  mapsnf1o2  8901  canth2  9128  1sdom2  9218  unfilem2  9276  cantnfvalf  9644  cnfcom3clem  9684  ssttrcl  9694  tc2  9719  r111  9757  rankf  9776  cardf2  9948  harcard  9983  r0weon  10015  infxpenc  10021  infxpenc2lem1  10022  alephon  10072  alephf1  10088  alephiso  10101  alephsmo  10105  alephf1ALT  10106  alephfplem4  10110  ackbij1lem17  10237  ackbij1  10239  ackbij2  10244  fin1a2lem2  10403  fin1a2lem4  10405  axcc2lem  10438  iunfo  10541  smobeth  10589  0tsk  10758  1pi  10886  nqerf  10933  axaddf  11148  axmulf  11149  axicn  11153  mpoaddf  11212  mpomulf  11213  mulnzcnf  11878  negiso  12213  dfnn2  12264  nnind  12269  0z  12620  dfuzi  12705  cnref1o  13027  elrpii  13037  0e0icopnf  13503  0e0iccpnf  13504  fldiv4p1lem1div2  13888  om2uzf1oi  14009  om2uzisoi  14010  uzrdgfni  14014  expcl2lem  14129  expclzlem  14139  expge0  14154  expge1  14155  faclbnd4lem1  14349  hashkf  14388  wwlktovf1  15020  sgnfo  15162  sqrtf  15441  fclim  15630  fprodn0f  16071  eff2  16180  reeff1  16201  ef01bndlem  16265  sin01bnd  16266  cos01bnd  16267  sin01gt0  16271  egt2lt3  16287  qnnen  16294  ruc  16324  halfleoddlt  16445  divalglem2  16478  divalglem9  16484  bitsf1  16529  sadaddlem  16549  2prm  16775  3prm  16777  1arith  17012  prmlem1a  17191  setsnid  17293  xpsff1o  17646  dmaf  18131  cdaf  18132  coapm  18153  0pos  18402  isposi  18404  letsr  18674  ex-chn1  18718  ex-chn2  18719  sgrp0b  18815  frmdplusg  18944  efmndsgrp  18976  smndex1sgrp  19001  smndex1mnd  19003  symg2bas  19494  pmtrsn  19620  odf  19638  efgsfo  19840  efgrelexlemb  19851  isabli  19897  rngmgpf  20266  mgpf  20361  prdscrngd  20436  xrsmgmdifsgrp  21596  cnmgpid  21616  xrs1cmn  21629  xrge0omnd  21632  zringnzr  21647  zringunit  21653  zringlpir  21654  zringndrg  21655  pzriprnglem5  21672  pzriprnglem7  21674  pzriprnglem9  21676  pzriprnglem13  21680  zzngim  21739  cnmsgngrp  21766  psgninv  21769  zrhpsgnmhm  21771  retos  21805  refld  21806  rzgrp  21810  pjpm  21895  fntopon  23118  istpsi  23136  cmpfi  23602  indisconn  23612  kqf  23941  fbssfi  24031  zfbas  24090  ptcmplem2  24247  prdstmdd  24318  tsmsfbas  24322  ismeti  24519  prdsxmslem2  24723  cnfldms  24969  cnnrg  24974  tgqioo  24994  xrtgioo  25001  recld2  25009  xrge0gsumle  25028  xrge0tsms  25029  addcnlem  25059  divcn  25064  abscncf  25097  recncf  25098  imcncf  25099  cjcncf  25100  icopnfhmeo  25139  xrhmeo  25142  cnllycmp  25152  isclmi0  25294  iscvsi  25325  cnstrcvs  25337  cncms  25551  ovolf  25678  ovolre  25721  opnmblALT  25799  dveflem  26175  mdegxrf  26262  iaa  26525  ulmdm  26593  dvradcnv  26621  reeff1o  26647  reefiso  26648  reefgim  26650  recosf1o  26737  efifo  26749  logcn  26849  cxpcn3  26950  resqrtcn  26951  logb1  26971  logbmpt  26990  2logb9irrALT  27000  sqrt2cxp2logb9e3  27001  ressatans  27136  lgamcvg2  27256  lgam1  27265  gam1  27266  efnnfsumcl  27304  efchtdvds  27360  ppiub  27405  lgslem2  27499  lgsfcl2  27504  lgsne0  27536  2lgslem1b  27593  padicabvf  27832  bdayfo  27878  cutsf  28022  madef  28066  cutsfo  28135  addsf  28212  addsfo  28213  negsf  28282  negsfo  28283  negsf1o  28284  subsfo  28295  0ons  28486  1ons  28487  oniso  28501  dfn0s2  28562  1nns  28579  bdayn0sf1o  28600  zsoring  28639  twocut  28653  0reno  28726  1reno  28727  istrkg3ld  28767  axlowdimlem16  29344  upgrbi  29480  umgrbi  29488  lfuhgr1v0e  29641  cusgr0  29813  wlk2v2elem2  30544  upgr4cycl4dv4e  30573  konigsberglem4  30643  frgr0  30653  ex-pss  30816  ex-fl  30835  ex-mod  30837  isgrpoi  30887  grporn  30910  isabloi  30940  smcnlem  31086  lnocoi  31146  cncph  31208  cnbn  31258  cnchl  31305  norm3adifii  31537  hhph  31567  hhhl  31593  hlim0  31624  hlimf  31626  helch  31632  hsn0elch  31637  hhssabloilem  31650  hhssnv  31653  hhshsslem2  31657  hhssbnOLD  31668  shscli  31706  shintcli  31718  chintcli  31720  shsval2i  31776  pjhthlem2  31781  lejdii  31927  nonbooli  32040  pjrni  32091  pjfoi  32092  pjfi  32093  pjmf1  32105  df0op2  32141  idunop  32367  0cnop  32368  0cnfn  32369  idcnop  32370  idhmop  32371  0hmop  32372  0lnfn  32374  0bdop  32382  lnophsi  32390  lnopcoi  32392  lnopunii  32401  lnophmi  32407  nmcopex  32418  nmcoplb  32419  nmcfnex  32442  nmcfnlb  32443  imaelshi  32447  nlelshi  32449  nlelchi  32450  riesz4i  32452  riesz4  32453  riesz1  32454  cnlnadjlem6  32461  cnlnadjlem9  32464  cnlnadjeui  32466  cnlnadjeu  32467  nmopadji  32479  bdophsi  32485  bdopcoi  32487  nmopcoadji  32490  pjhmopi  32535  pjbdlni  32538  hmopidmchi  32540  mdslj1i  32708  rinvf1o  33012  nnindf  33201  rpdp2cl  33238  dp2ltc  33243  dpmul4  33270  s3clhash  33302  xrstos  33361  xrsclat  33362  xrge0tsmsd  33424  qfld  33649  cnfldfld  33693  reofld  33694  nn0archi  33698  zringidom  33872  zringfrac  33875  ccfldextrr  34067  ccfldsrarelvec  34092  ccfldextdgrr  34093  2sqr3minply  34201  xrge0iifmhm  34360  xrge0pluscn  34361  cnzh  34389  rezh  34390  qqhval2lem  34402  esum0  34470  esumcst  34484  esumpcvgval  34499  esumcvg  34507  dmvlsiga  34550  measdivcstALTV  34647  eulerpartlemt  34793  coinfliprv  34905  ballotlem2  34911  signswmnd  34976  logdivsqrle  35069  hgt750lem  35070  bnj906  35350  xoromon  35504  rankfo  35530  fineqvnttrclse  35561  indispconn  35747  cnllysconn  35758  rellysconn  35764  msrf  36055  brbigcup  36409  fobigcup  36411  brsingle  36428  fnsingle  36430  brimage  36437  funimage  36439  fnimage  36440  imageval  36441  brcart  36443  brapply  36449  brcup  36450  brcap  36451  funpartfun  36456  brub  36467  mpomulnzcnf  36852  onsucconni  36989  onsucsuccmpi  36995  dnicn  37122  bj-nnfv  37434  bj-wnfnf  37449  bj-nnfa1  37450  bj-nnfe1  37451  bj-rabtr  37607  bj-axreprepsep  37753  taupilem2  38007  taupi  38008  f1omptsnlem  38023  icoreresf  38039  relowlpssretop  38051  finxpreclem3  38080  matunitlindf  38310  mblfinlem2  38350  areacirc  38405  0totbnd  38465  heiborlem6  38508  dfsucmap3  39153  refrelid  39292  idsymrel  39335  trrelressn  39357  refrelsredund4  39406  refrelredund4  39409  disjALTV0  39544  disjALTVid  39545  antisymrelressn  39557  isolatiN  40031  isomliN  40054  ishlatiN  40170  mzpclall  43499  jm2.20nn  43765  dfacbasgrp  43876  dgraaf  43915  onexoegt  44012  omnord1  44073  oege2  44075  oenord1  44084  cantnftermord  44088  cantnf2  44093  omabs2  44100  omcl2  44101  ifpim3  44263  ifpim4  44265  ifpbi1b  44270  eu0  44287  omiscard  44310  iso0  45058  dvsid  45082  rankrelp  45710  hashomiso  45775  halffl  46056  resincncf  46630  0cnf  46632  iblempty  46720  dirkeritg  46857  fourierdlem62  46923  fourierdlem76  46937  fourierdlem103  46964  etransclem18  47007  etransclem46  47035  abnotbtaxb  47693  dfaiota3  47870  ceilhalf1  48116  sprsymrelf1  48286  fmtnof1  48328  fmtno4prm  48368  prmdvdsfmtnof1  48380  31prm  48390  requad01  48427  0evenALTV  48494  1oddALTV  48496  2evenALTV  48498  6even  48517  8even  48519  6gbe  48577  7gbow  48578  8gbe  48579  9gbo  48580  11gbo  48581  usgrexmpl1lem  48827  usgrexmpl2lem  48832  usgrexmpl2trifr  48843  gpg5grlim  48899  gpg5grlic  48900  uspgrsprf1  48953  1odd  48977  nnsgrp  48983  0even  49043  2even  49045  2zrngamgm  49051  2zrngasgrp  49052  2zrngamnd  49053  2zrngagrp  49055  2zrngmsgrp  49059  zlmodzxzldeplem3  49323  lvecpsslmod  49328  ldepsnlinc  49329  blennngt2o2  49413  blennn0e2  49415  ackval42  49517  rrx2xpref1o  49539  rrx2plordisom  49544  slotresfo  49718  sepfsepc  49747  basresposfo  49797  oppff1  49967  setcsnterm  50309  setc1onsubc  50421  setrec2lem2  50513  aacllem  50662  2elfz13  50667