Theorem mpbir2an 701

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)

Hypotheses

Ref	Expression
mpbir2an.1	⊢ 𝜓
mpbir2an.2	⊢ 𝜒
mpbiran2an.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbir2an	⊢ 𝜑

Proof of Theorem mpbir2an

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 ⊢ 𝜒
2		mpbir2an.1	. . 3 ⊢ 𝜓
3		mpbiran2an.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
4	2, 3	mpbiran 699	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 223	1 ⊢ 𝜑

Syntax hints:   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  3pm3.2i  1395  euequ  2615  eqssi  3836  elini  4019  dtru  5082  opnzi  5174  so0  5309  we0  5350  difxp  5812  ord0  6028  dfiota4  6127  funi  6167  funcnvsn  6184  fnresi  6254  fn0  6257  f0  6336  fconst  6341  f10  6423  f1o0  6427  f1oi  6428  f1osn  6430  isoid  6851  porpss  7218  epweon  7260  ordon  7261  omssnlim  7357  fo1st  7465  fo2nd  7466  wfrfun  7708  wfr1  7716  iordsmo  7737  tfrlem7  7762  tfr1  7776  frfnom  7813  seqomlem2  7829  oawordeulem  7918  mapsnf1o2  8191  canth2  8401  unfilem2  8513  cantnfvalf  8859  cnfcom3clem  8899  tc2  8915  r111  8935  rankf  8954  cardf2  9102  harcard  9137  r0weon  9168  infxpenc  9174  infxpenc2lem1  9175  alephon  9225  alephf1  9241  alephiso  9254  alephsmo  9258  alephf1ALT  9259  alephfplem4  9263  ackbij1lem17  9393  ackbij1  9395  ackbij2  9400  fin1a2lem2  9558  fin1a2lem4  9560  axcc2lem  9593  iunfo  9696  smobeth  9743  0tsk  9912  1pi  10040  nqerf  10087  axaddf  10302  axmulf  10303  axicn  10307  mulnzcnopr  11021  negiso  11357  dfnn2  11389  nnind  11394  0z  11739  dfuzi  11820  cnref1o  12132  elrpii  12140  0e0icopnf  12596  0e0iccpnf  12597  fz0to4untppr  12761  fldiv4p1lem1div2  12955  om2uzf1oi  13071  om2uzisoi  13072  uzrdgfni  13076  expcl2lem  13190  expclzlem  13202  expge0  13214  expge1  13215  faclbnd4lem1  13398  hashkf  13437  wwlktovf1  14109  sqrtf  14510  fclim  14692  fprodn0f  15124  eff2  15231  reeff1  15252  ef01bndlem  15316  sin01bnd  15317  cos01bnd  15318  sin01gt0  15322  egt2lt3  15338  qnnen  15346  ruc  15376  halfleoddlt  15490  divalglem2  15525  divalglem9  15531  bitsf1  15574  sadaddlem  15594  2prm  15810  3prm  15811  1arith  16035  prmlem1a  16212  setsnid  16311  xpsff1o  16614  dmaf  17084  cdaf  17085  coapm  17106  0pos  17340  isposi  17342  fpwipodrs  17550  letsr  17613  sgrp0b  17678  frmdplusg  17778  symg2bas  18201  pmtrsn  18323  odf  18340  efgsfo  18537  efgrelexlemb  18549  isabli  18593  mgpf  18946  prdscrngd  19000  xrsmgmdifsgrp  20179  xrs1cmn  20182  cnmgpid  20204  zringnzr  20226  zringunit  20232  zringlpir  20233  zringndrg  20234  zzngim  20296  cnmsgngrp  20320  psgninv  20323  zrhpsgnmhm  20325  retos  20361  refld  20362  rzgrp  20366  pjpm  20451  fntopon  21136  istpsi  21154  0cmp  21606  cmpfi  21620  indisconn  21630  comppfsc  21744  kqf  21959  ptcmpfi  22025  fbssfi  22049  zfbas  22108  alexsubALTlem2  22260  alexsubALTlem4  22262  ptcmplem2  22265  ptcmp  22270  prdstmdd  22335  tsmsfbas  22339  ismeti  22538  prdsxmslem2  22742  cnfldms  22987  cnnrg  22992  tgqioo  23011  xrtgioo  23017  recld2  23025  xrge0gsumle  23044  xrge0tsms  23045  addcnlem  23075  divcn  23079  abscncf  23112  recncf  23113  imcncf  23114  cjcncf  23115  icopnfhmeo  23150  xrhmeo  23153  cnllycmp  23163  isclmi0  23305  iscvsi  23336  cnstrcvs  23348  cncvs  23352  cncms  23561  ovolf  23686  ovolicc1  23720  ovolre  23729  ioorf  23777  opnmblALT  23807  dveflem  24179  mdegxrf  24265  iaa  24517  ulmdm  24584  dvradcnv  24612  reeff1o  24638  reefiso  24639  reefgim  24641  recosf1o  24719  efifo  24731  logcn  24830  cxpcn3  24929  resqrtcn  24930  logb1  24947  logbmpt  24966  2logb9irrALT  24976  sqrt2cxp2logb9e3  24977  ressatans  25112  lgamcvg2  25233  lgam1  25242  gam1  25243  efnnfsumcl  25281  efchtdvds  25337  ppiub  25381  lgslem2  25475  lgsfcl2  25480  lgsne0  25512  2lgslem1b  25569  padicabvf  25772  istrkg3ld  25812  axlowdimlem16  26306  upgrbi  26441  umgrbi  26449  lfuhgr1v0e  26601  cusgr0  26774  wlk2v2elem2  27559  upgr4cycl4dv4e  27588  konigsberglem4  27661  frgr0  27672  ex-pss  27860  ex-fl  27879  isgrpoi  27925  grporn  27948  isabloi  27978  smcnlem  28124  lnocoi  28184  cncph  28246  cnbn  28297  cnchl  28344  norm3adifii  28577  hhph  28607  hhhl  28633  hlim0  28664  hlimf  28666  helch  28672  hsn0elch  28677  hhssabloilem  28690  hhssnv  28693  hhshsslem2  28697  hhssbnOLD  28709  hhsshlOLD  28710  shscli  28748  shintcli  28760  chintcli  28762  shsval2i  28818  pjhthlem2  28823  lejdii  28969  nonbooli  29082  pjrni  29133  pjfoi  29134  pjfi  29135  pjmf1  29147  df0op2  29183  idunop  29409  0cnop  29410  0cnfn  29411  idcnop  29412  idhmop  29413  0hmop  29414  0lnfn  29416  0bdop  29424  lnophsi  29432  lnopcoi  29434  lnopunii  29443  lnophmi  29449  nmcopex  29460  nmcoplb  29461  nmcfnex  29484  nmcfnlb  29485  imaelshi  29489  nlelshi  29491  nlelchi  29492  riesz4i  29494  riesz4  29495  riesz1  29496  cnlnadjlem6  29503  cnlnadjlem9  29506  cnlnadjeui  29508  cnlnadjeu  29509  nmopadji  29521  bdophsi  29527  bdopcoi  29529  nmopcoadji  29532  pjhmopi  29577  pjbdlni  29580  hmopidmchi  29582  mdslj1i  29750  rinvf1o  29997  nnindf  30129  rpdp2cl  30152  dp2ltc  30157  dpmul4  30184  xrstos  30241  xrsclat  30242  xrge0omnd  30273  xrge0tsmsd  30347  reofld  30402  nn0archi  30405  xrge0iifmhm  30583  xrge0pluscn  30584  cnzh  30612  rezh  30613  qqhval2lem  30623  esum0  30709  esumcst  30723  esumpcvgval  30738  esumcvg  30746  dmvlsiga  30790  measdivcstOLD  30885  eulerpartlemt  31031  coinfliprv  31143  ballotlem2  31149  signswmnd  31234  logdivsqrle  31330  hgt750lem  31331  bnj906  31599  indispconn  31815  cnllysconn  31826  rellysconn  31832  msrf  32038  soseq  32343  frrlem5c  32375  bdayfo  32417  scutf  32508  brbigcup  32594  fobigcup  32596  brsingle  32613  fnsingle  32615  brimage  32622  funimage  32624  fnimage  32625  imageval  32626  brcart  32628  brapply  32634  brcup  32635  brcap  32636  funpartfun  32639  brub  32650  onsucconni  33019  onsucsuccmpi  33025  dnicn  33065  bj-dtru  33373  bj-rabtr  33500  taupilem2  33764  taupi  33765  f1omptsnlem  33779  icoreresf  33795  relowlpssretop  33807  finxpreclem3  33825  matunitlindf  34028  mblfinlem2  34068  areacirc  34125  0totbnd  34191  heiborlem6  34234  refrelid  34894  idsymrel  34930  refrelsred4  34996  refrelred4  34999  isolatiN  35365  isomliN  35388  ishlatiN  35504  sbtv  38114  mzpclall  38243  jm2.20nn  38516  dfacbasgrp  38630  dgraaf  38669  ifpim3  38792  ifpim4  38794  ifpbi1b  38799  iso0  39455  dvsid  39479  halffl  40412  resincncf  41009  0cnf  41011  iblempty  41101  dirkeritg  41239  fourierdlem62  41305  fourierdlem76  41319  fourierdlem103  41346  etransclem18  41389  etransclem46  41417  abnotbtaxb  42002  sprsymrelf1  42428  fmtnof1  42461  fmtno4prm  42501  prmdvdsfmtnof1  42513  31prm  42526  requad01  42552  0evenALTV  42617  1oddALTV  42619  2evenALTV  42621  6even  42638  8even  42640  6gbe  42677  7gbow  42678  8gbe  42679  9gbo  42680  11gbo  42681  uspgrsprf1  42763  1odd  42819  nnsgrp  42825  0even  42939  2even  42941  2zrngamgm  42947  2zrngasgrp  42948  2zrngamnd  42949  2zrngagrp  42951  2zrngmsgrp  42955  zlmodzxzldeplem3  43299  lvecpsslmod  43304  ldepsnlinc  43305  blennngt2o2  43394  blennn0e2  43396  rrx2xpref1o  43447  rrx2plordisom  43452  setrec2lem2  43539  aacllem  43646