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  2622  eqssi  3924  elini  4096  dtruALT2  5331  exexneq  5402  opnzi  5442  so0  5596  we0  5645  difxp  6154  ord0  6417  dfiota4  6530  funi  6572  funcnvsn  6590  idfn  6667  fn0  6670  f0  6763  fconst  6768  f10  6858  f1o0  6862  f1oiOLD  6864  f1osn  6866  isoid  7337  porpss  7743  epweon  7789  epweonALT  7790  ordon  7791  omssnlim  7892  peano1  7900  fo1st  8021  fo2nd  8022  soseq  8178  iordsmo  8368  tfrlem7  8394  tfr1  8408  frfnom  8446  seqomlem2  8464  oawordeulem  8565  1onn  8652  2onn  8654  naddf  8694  mapsnf1o2  8925  canth2  9152  1sdom2  9242  unfilem2  9301  cantnfvalf  9669  cnfcom3clem  9709  ssttrcl  9719  tc2  9744  r111  9785  rankf  9805  setrec2lem2  9979  cardf2  10027  harcard  10062  r0weon  10094  infxpenc  10100  infxpenc2lem1  10101  alephon  10151  alephf1  10167  alephiso  10180  alephsmo  10184  alephf1ALT  10185  alephfplem4  10189  ackbij1lem17  10316  ackbij1  10318  ackbij2  10323  fin1a2lem2  10482  fin1a2lem4  10484  axcc2lem  10517  iunfo  10626  smobeth  10674  0tsk  10843  1pi  10971  nqerf  11018  axaddf  11233  axmulf  11234  axicn  11238  mpoaddf  11297  mpomulf  11298  mulnzcnf  11965  negiso  12300  dfnn2  12351  nnind  12356  0z  12707  dfuzi  12793  cnref1o  13116  elrpii  13126  0e0icopnf  13592  0e0iccpnf  13593  fldiv4p1lem1div2  13978  om2uzf1oi  14099  om2uzisoi  14100  uzrdgfni  14104  expcl2lem  14219  expclzlem  14229  expge0  14244  expge1  14245  faclbnd4lem1  14440  hashkf  14479  wwlktovf1  15115  sgnfo  15257  sqrtf  15536  fclim  15725  fprodn0f  16163  eff2  16272  reeff1  16293  ef01bndlem  16357  sin01bnd  16358  cos01bnd  16359  sin01gt0  16363  egt2lt3  16379  qnnen  16386  ruc  16416  halfleoddlt  16537  divalglem2  16570  divalglem9  16576  bitsf1  16621  sadaddlem  16641  2prm  16872  3prm  16874  1arith  17110  prmlem1a  17289  setsnid  17391  xpsff1o  17744  dmaf  18229  cdaf  18230  coapm  18251  0pos  18500  isposi  18502  letsr  18772  ex-chn1  18816  ex-chn2  18817  sgrp0b  18922  frmdplusg  19055  efmndsgrp  19087  smndex1sgrp  19112  smndex1mnd  19114  symg2bas  19612  pmtrsn  19738  odf  19756  efgsfo  19958  efgrelexlemb  19969  isabli  20015  rngmgpf  20384  mgpf  20480  prdscrngd  20556  xrsmgmdifsgrp  21720  cnmgpid  21740  xrs1cmn  21753  xrge0omnd  21756  zringnzr  21771  zringunit  21777  zringlpir  21778  zringndrg  21779  pzriprnglem5  21796  pzriprnglem7  21798  pzriprnglem9  21800  pzriprnglem13  21804  zzngim  21863  cnmsgngrp  21890  psgninv  21893  zrhpsgnmhm  21895  retos  21929  refld  21930  rzgrp  21934  pjpm  22019  matunitlindf  23001  fntopon  23247  istpsi  23265  cmpfi  23731  indisconn  23741  kqf  24071  fbssfi  24161  zfbas  24220  ptcmplem2  24377  prdstmdd  24448  tsmsfbas  24452  ismeti  24649  prdsxmslem2  24853  cnfldms  25099  cnnrg  25104  tgqioo  25124  xrtgioo  25131  recld2  25139  xrge0gsumle  25158  xrge0tsms  25159  addcnlem  25189  divcn  25194  abscncf  25227  recncf  25228  imcncf  25229  cjcncf  25230  icopnfhmeo  25269  xrhmeo  25272  cnllycmp  25282  isclmi0  25424  iscvsi  25455  cnstrcvs  25467  cncms  25681  ovolf  25808  ovolre  25851  opnmblALT  25929  dveflem  26304  mdegxrf  26391  iaaOLD  26657  ulmdm  26725  dvradcnv  26753  reeff1o  26779  reefiso  26780  reefgim  26782  recosf1o  26868  efifo  26880  logcn  26980  cxpcn3  27081  resqrtcn  27082  logb1  27102  logbmpt  27121  2logb9irrALT  27131  sqrt2cxp2logb9e3  27132  ressatans  27267  lgamcvg2  27387  lgam1  27396  gam1  27397  efnnfsumcl  27435  efchtdvds  27491  ppiub  27536  lgslem2  27630  lgsfcl2  27635  lgsne0  27667  2lgslem1b  27724  padicabvf  27963  bdayfo  28039  cutsf  28183  madef  28227  cutsfo  28296  addsf  28373  addsfo  28374  negsf  28443  negsfo  28444  negsf1o  28445  subsfo  28456  0ons  28647  1ons  28648  oniso  28662  dfn0s2  28723  1nns  28740  bdayn0sf1o  28761  zsoring  28800  twocut  28814  0reno  28887  1reno  28888  istrkg3ld  28928  axlowdimlem16  29540  upgrbi  29676  umgrbi  29684  lfuhgr1v0e  29840  cusgr0  30012  wlk2v2elem2  30762  upgr4cycl4dv4e  30791  konigsberglem4  30861  frgr0  30871  ex-pss  31034  ex-fl  31053  ex-mod  31055  isgrpoi  31105  grporn  31128  isabloi  31158  smcnlem  31304  lnocoi  31364  cncph  31426  cnbn  31476  cnchl  31523  norm3adifii  31755  hhph  31785  hhhl  31811  hlim0  31842  hlimf  31844  helch  31850  hsn0elch  31855  hhssabloilem  31868  hhssnv  31871  hhshsslem2  31875  hhssbnOLD  31886  shscli  31924  shintcli  31936  chintcli  31938  shsval2i  31994  pjhthlem2  31999  lejdii  32145  nonbooli  32258  pjrni  32309  pjfoi  32310  pjfi  32311  pjmf1  32323  df0op2  32359  idunop  32585  0cnop  32586  0cnfn  32587  idcnop  32588  idhmop  32589  0hmop  32590  0lnfn  32592  0bdop  32600  lnophsi  32608  lnopcoi  32610  lnopunii  32619  lnophmi  32625  nmcopex  32636  nmcoplb  32637  nmcfnex  32660  nmcfnlb  32661  imaelshi  32665  nlelshi  32667  nlelchi  32668  riesz4i  32670  riesz4  32671  riesz1  32672  cnlnadjlem6  32679  cnlnadjlem9  32682  cnlnadjeui  32684  cnlnadjeu  32685  nmopadji  32697  bdophsi  32703  bdopcoi  32705  nmopcoadji  32708  pjhmopi  32753  pjbdlni  32756  hmopidmchi  32758  mdslj1i  32926  rinvf1o  33271  nnindf  33457  rpdp2cl  33494  dp2ltc  33499  dpmul4  33526  s3clhash  33558  xrstos  33617  xrsclat  33618  xrge0tsmsd  33680  qfld  33905  cnfldfld  33949  reofld  33950  nn0archi  33954  zringidom  34129  zringfrac  34132  ccfldextrr  34324  ccfldsrarelvec  34349  ccfldextdgrr  34350  2sqr3minply  34458  xrge0iifmhm  34617  xrge0pluscn  34618  cnzh  34646  rezh  34647  qqhval2lem  34659  esum0  34727  esumcst  34741  esumpcvgval  34756  esumcvg  34764  dmvlsiga  34807  measdivcstALTV  34904  eulerpartlemt  35049  coinfliprv  35161  ballotlem2  35167  signswmnd  35232  logdivsqrle  35325  hgt750lem  35326  bnj906  35606  xoromon  35767  rankfo  35787  fineqvnttrclse  35848  indispconn  36085  cnllysconn  36096  rellysconn  36102  msrf  36393  onprcr  36548  brbigcup  36752  fobigcup  36754  brsingle  36771  fnsingle  36773  brimage  36780  funimage  36782  fnimage  36783  imageval  36784  brcart  36786  brapply  36792  brcup  36793  brcap  36794  funpartfun  36799  brub  36810  mpomulnzcnf  37180  onsucconni  37317  onsucsuccmpi  37323  dnicn  37450  bj-nnfv  37762  bj-wnfnf  37777  bj-nnfa1  37778  bj-nnfe1  37779  bj-rabtr  37935  bj-axreprepsep  38083  taupilem2  38336  taupi  38337  f1omptsnlem  38352  icoreresf  38368  relowlpssretop  38380  finxpreclem3  38409  mblfinlem2  38669  areacirc  38724  0totbnd  38800  heiborlem6  38843  dfsucmap3  39488  refrelid  39627  idsymrel  39670  trrelressn  39692  refrelsredund4  39741  refrelredund4  39744  disjALTV0  39879  disjALTVid  39880  antisymrelressn  39892  isolatiN  40366  isomliN  40389  ishlatiN  40505  mzpclall  43831  jm2.20nn  44097  dfacbasgrp  44203  dgraaf  44242  onexoegt  44339  omnord1  44400  oege2  44402  oenord1  44411  cantnftermord  44415  cantnf2  44420  omabs2  44427  omcl2  44428  ifpim3  44590  ifpim4  44592  ifpbi1b  44597  eu0  44614  omiscard  44637  iso0  45384  dvsid  45408  rankrelp  46043  hashomiso  46108  halffl  46405  resincncf  46978  0cnf  46980  iblempty  47068  dirkeritg  47205  fourierdlem62  47271  fourierdlem76  47285  fourierdlem103  47312  etransclem18  47355  etransclem46  47383  sinnpoly  48034  abnotbtaxb  48078  dfaiota3  48255  ceilhalf1  48501  sprsymrelf1  48671  fmtnof1  48713  fmtno4prm  48753  prmdvdsfmtnof1  48765  31prm  48775  requad01  48812  0evenALTV  48879  1oddALTV  48881  2evenALTV  48883  6even  48902  8even  48904  6gbe  48962  7gbow  48963  8gbe  48964  9gbo  48965  11gbo  48966  usgrexmpl1lem  49212  usgrexmpl2lem  49217  usgrexmpl2trifr  49228  gpg5grlim  49284  gpg5grlic  49285  uspgrsprf1  49338  1odd  49361  nnsgrp  49367  0even  49427  2even  49429  2zrngamgm  49435  2zrngasgrp  49436  2zrngamnd  49437  2zrngagrp  49439  2zrngmsgrp  49443  zlmodzxzldeplem3  49707  lvecpsslmod  49712  ldepsnlinc  49713  blennngt2o2  49797  blennn0e2  49799  ackval42  49901  rrx2plordisom  49929  slotresfo  50106  sepfsepc  50135  basresposfo  50185  oppff1  50357  setcsnterm  50718  setc1onsubc  50833  aacllem  51107  veroquadmodzerod  51152  veroquadnolindfd  51153