Theorem mpbir2an 710

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

Syntax hints:   ↔ wb 209   ∧ 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 210  df-an 400

This theorem is referenced by:  3pm3.2i  1336  euequ  2658  eqssi  3931  elini  4120  dtru  5236  opnzi  5331  so0  5473  we0  5514  difxp  5988  ord0  6211  dfiota4  6316  funi  6356  funcnvsn  6374  idfn  6447  fnresiOLD  6449  fn0  6451  f0  6534  fconst  6539  f10  6622  f1o0  6626  f1oi  6627  f1osn  6629  isoid  7061  porpss  7433  epweon  7477  ordon  7478  omssnlim  7574  fo1st  7691  fo2nd  7692  wfrfun  7948  wfr1  7956  iordsmo  7977  tfrlem7  8002  tfr1  8016  frfnom  8053  seqomlem2  8070  oawordeulem  8163  mapsnf1o2  8441  canth2  8654  unfilem2  8767  cantnfvalf  9112  cnfcom3clem  9152  tc2  9168  r111  9188  rankf  9207  cardf2  9356  harcard  9391  r0weon  9423  infxpenc  9429  infxpenc2lem1  9430  alephon  9480  alephf1  9496  alephiso  9509  alephsmo  9513  alephf1ALT  9514  alephfplem4  9518  ackbij1lem17  9647  ackbij1  9649  ackbij2  9654  fin1a2lem2  9812  fin1a2lem4  9814  axcc2lem  9847  iunfo  9950  smobeth  9997  0tsk  10166  1pi  10294  nqerf  10341  axaddf  10556  axmulf  10557  axicn  10561  mulnzcnopr  11275  negiso  11608  dfnn2  11638  nnind  11643  0z  11980  dfuzi  12061  cnref1o  12372  elrpii  12380  0e0icopnf  12836  0e0iccpnf  12837  fz0to4untppr  13005  fldiv4p1lem1div2  13200  om2uzf1oi  13316  om2uzisoi  13317  uzrdgfni  13321  expcl2lem  13437  expclzlem  13449  expge0  13461  expge1  13462  faclbnd4lem1  13649  hashkf  13688  wwlktovf1  14312  sqrtf  14715  fclim  14902  fprodn0f  15337  eff2  15444  reeff1  15465  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  sin01gt0  15535  egt2lt3  15551  qnnen  15558  ruc  15588  halfleoddlt  15703  divalglem2  15736  divalglem9  15742  bitsf1  15785  sadaddlem  15805  2prm  16026  3prm  16028  1arith  16253  prmlem1a  16432  setsnid  16531  xpsff1o  16832  dmaf  17301  cdaf  17302  coapm  17323  0pos  17556  isposi  17558  letsr  17829  sgrp0b  17901  frmdplusg  18011  efmndsgrp  18043  smndex1sgrp  18065  smndex1mnd  18067  symg2bas  18513  pmtrsn  18639  odf  18657  efgsfo  18857  efgrelexlemb  18868  isabli  18913  mgpf  19305  prdscrngd  19359  xrsmgmdifsgrp  20128  xrs1cmn  20131  cnmgpid  20153  zringnzr  20175  zringunit  20181  zringlpir  20182  zringndrg  20183  zzngim  20244  cnmsgngrp  20268  psgninv  20271  zrhpsgnmhm  20273  retos  20307  refld  20308  rzgrp  20312  pjpm  20397  fntopon  21529  istpsi  21547  cmpfi  22013  indisconn  22023  kqf  22352  fbssfi  22442  zfbas  22501  ptcmplem2  22658  prdstmdd  22729  tsmsfbas  22733  ismeti  22932  prdsxmslem2  23136  cnfldms  23381  cnnrg  23386  tgqioo  23405  xrtgioo  23411  recld2  23419  xrge0gsumle  23438  xrge0tsms  23439  addcnlem  23469  divcn  23473  abscncf  23506  recncf  23507  imcncf  23508  cjcncf  23509  icopnfhmeo  23548  xrhmeo  23551  cnllycmp  23561  isclmi0  23703  iscvsi  23734  cnstrcvs  23746  cncms  23959  ovolf  24086  ovolre  24129  opnmblALT  24207  dveflem  24582  mdegxrf  24669  iaa  24921  ulmdm  24988  dvradcnv  25016  reeff1o  25042  reefiso  25043  reefgim  25045  recosf1o  25127  efifo  25139  logcn  25238  cxpcn3  25337  resqrtcn  25338  logb1  25355  logbmpt  25374  2logb9irrALT  25384  sqrt2cxp2logb9e3  25385  ressatans  25520  lgamcvg2  25640  lgam1  25649  gam1  25650  efnnfsumcl  25688  efchtdvds  25744  ppiub  25788  lgslem2  25882  lgsfcl2  25887  lgsne0  25919  2lgslem1b  25976  padicabvf  26215  istrkg3ld  26255  axlowdimlem16  26751  upgrbi  26886  umgrbi  26894  lfuhgr1v0e  27044  cusgr0  27216  wlk2v2elem2  27941  upgr4cycl4dv4e  27970  konigsberglem4  28040  frgr0  28050  ex-pss  28213  ex-fl  28232  ex-mod  28234  isgrpoi  28281  grporn  28304  isabloi  28334  smcnlem  28480  lnocoi  28540  cncph  28602  cnbn  28652  cnchl  28699  norm3adifii  28931  hhph  28961  hhhl  28987  hlim0  29018  hlimf  29020  helch  29026  hsn0elch  29031  hhssabloilem  29044  hhssnv  29047  hhshsslem2  29051  hhssbnOLD  29062  shscli  29100  shintcli  29112  chintcli  29114  shsval2i  29170  pjhthlem2  29175  lejdii  29321  nonbooli  29434  pjrni  29485  pjfoi  29486  pjfi  29487  pjmf1  29499  df0op2  29535  idunop  29761  0cnop  29762  0cnfn  29763  idcnop  29764  idhmop  29765  0hmop  29766  0lnfn  29768  0bdop  29776  lnophsi  29784  lnopcoi  29786  lnopunii  29795  lnophmi  29801  nmcopex  29812  nmcoplb  29813  nmcfnex  29836  nmcfnlb  29837  imaelshi  29841  nlelshi  29843  nlelchi  29844  riesz4i  29846  riesz4  29847  riesz1  29848  cnlnadjlem6  29855  cnlnadjlem9  29858  cnlnadjeui  29860  cnlnadjeu  29861  nmopadji  29873  bdophsi  29879  bdopcoi  29881  nmopcoadji  29884  pjhmopi  29929  pjbdlni  29932  hmopidmchi  29934  mdslj1i  30102  rinvf1o  30389  nnindf  30561  rpdp2cl  30584  dp2ltc  30589  dpmul4  30616  s3clhash  30650  xrstos  30713  xrsclat  30714  xrge0tsmsd  30742  xrge0omnd  30762  reofld  30964  nn0archi  30967  ccfldextrr  31126  ccfldsrarelvec  31144  ccfldextdgrr  31145  xrge0iifmhm  31292  xrge0pluscn  31293  cnzh  31321  rezh  31322  qqhval2lem  31332  esum0  31418  esumcst  31432  esumpcvgval  31447  esumcvg  31455  dmvlsiga  31498  measdivcstALTV  31594  eulerpartlemt  31739  coinfliprv  31850  ballotlem2  31856  signswmnd  31937  logdivsqrle  32031  hgt750lem  32032  bnj906  32312  indispconn  32594  cnllysconn  32605  rellysconn  32611  msrf  32902  soseq  33209  bdayfo  33295  scutf  33386  brbigcup  33472  fobigcup  33474  brsingle  33491  fnsingle  33493  brimage  33500  funimage  33502  fnimage  33503  imageval  33504  brcart  33506  brapply  33512  brcup  33513  brcap  33514  funpartfun  33517  brub  33528  onsucconni  33898  onsucsuccmpi  33904  dnicn  33944  bj-wnfnf  34183  bj-nnfv  34198  bj-nnfa1  34203  bj-nnfe1  34204  bj-dtru  34254  bj-rabtr  34372  taupilem2  34736  taupi  34737  f1omptsnlem  34753  icoreresf  34769  relowlpssretop  34781  finxpreclem3  34810  matunitlindf  35055  mblfinlem2  35095  areacirc  35150  0totbnd  35211  heiborlem6  35254  refrelid  35921  idsymrel  35957  refrelsredund4  36027  refrelredund4  36030  disjALTV0  36144  disjALTVid  36145  isolatiN  36512  isomliN  36535  ishlatiN  36651  sn-dtru  39403  mzpclall  39668  jm2.20nn  39938  dfacbasgrp  40052  dgraaf  40091  ifpim3  40204  ifpim4  40206  ifpbi1b  40211  eu0  40228  iso0  41011  dvsid  41035  halffl  41928  resincncf  42517  0cnf  42519  iblempty  42607  dirkeritg  42744  fourierdlem62  42810  fourierdlem76  42824  fourierdlem103  42851  etransclem18  42894  etransclem46  42922  abnotbtaxb  43508  sprsymrelf1  44013  fmtnof1  44052  fmtno4prm  44092  prmdvdsfmtnof1  44104  31prm  44114  requad01  44139  0evenALTV  44206  1oddALTV  44208  2evenALTV  44210  6even  44229  8even  44231  6gbe  44289  7gbow  44290  8gbe  44291  9gbo  44292  11gbo  44293  uspgrsprf1  44375  1odd  44431  nnsgrp  44437  0even  44555  2even  44557  2zrngamgm  44563  2zrngasgrp  44564  2zrngamnd  44565  2zrngagrp  44567  2zrngmsgrp  44571  zlmodzxzldeplem3  44911  lvecpsslmod  44916  ldepsnlinc  44917  blennngt2o2  45006  blennn0e2  45008  ackval42  45110  rrx2xpref1o  45132  rrx2plordisom  45137  setrec2lem2  45224  aacllem  45329