Theorem mpbir2an 709

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

Syntax hints:   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  3pm3.2i  1336  euequ  2586  eqssi  3996  elini  4192  dtruALT2  5365  exexneq  5431  dtruOLD  5438  opnzi  5471  so0  5621  we0  5668  difxp  6166  ord0  6419  dfiota4  6536  funi  6581  funcnvsn  6599  idfn  6679  fn0  6682  f0  6773  fconst  6778  f10  6866  f1o0  6870  f1oi  6871  f1osn  6873  isoid  7331  porpss  7728  epweon  7773  epweonALT  7774  ordon  7775  omssnlim  7881  peano1  7890  fo1st  8013  fo2nd  8014  soseq  8163  wfrfunOLD  8339  wfr1OLD  8347  iordsmo  8377  tfrlem7  8403  tfr1  8417  frfnom  8455  seqomlem2  8471  oawordeulem  8574  1onn  8660  2onn  8662  naddf  8701  mapsnf1o2  8913  canth2  9158  1sdom2  9265  unfilem2  9336  cantnfvalf  9699  cnfcom3clem  9739  ssttrcl  9749  tc2  9776  r111  9809  rankf  9828  cardf2  9977  harcard  10012  r0weon  10046  infxpenc  10052  infxpenc2lem1  10053  alephon  10103  alephf1  10119  alephiso  10132  alephsmo  10136  alephf1ALT  10137  alephfplem4  10141  ackbij1lem17  10268  ackbij1  10270  ackbij2  10275  fin1a2lem2  10433  fin1a2lem4  10435  axcc2lem  10468  iunfo  10571  smobeth  10618  0tsk  10787  1pi  10915  nqerf  10962  axaddf  11177  axmulf  11178  axicn  11182  mpoaddf  11241  mpomulf  11242  mulnzcnf  11899  negiso  12238  dfnn2  12269  nnind  12274  0z  12613  dfuzi  12697  cnref1o  13013  elrpii  13023  0e0icopnf  13481  0e0iccpnf  13482  fz0to4untppr  13650  fldiv4p1lem1div2  13847  om2uzf1oi  13965  om2uzisoi  13966  uzrdgfni  13970  expcl2lem  14085  expclzlem  14095  expge0  14110  expge1  14111  faclbnd4lem1  14303  hashkf  14342  wwlktovf1  14959  sqrtf  15361  fclim  15548  fprodn0f  15986  eff2  16094  reeff1  16115  ef01bndlem  16179  sin01bnd  16180  cos01bnd  16181  sin01gt0  16185  egt2lt3  16201  qnnen  16208  ruc  16238  halfleoddlt  16357  divalglem2  16390  divalglem9  16396  bitsf1  16439  sadaddlem  16459  2prm  16686  3prm  16688  1arith  16922  prmlem1a  17102  setsnid  17204  setsnidOLD  17205  xpsff1o  17575  dmaf  18064  cdaf  18065  coapm  18086  0pos  18339  0posOLD  18340  isposi  18342  letsr  18611  sgrp0b  18714  frmdplusg  18837  efmndsgrp  18869  smndex1sgrp  18891  smndex1mnd  18893  symg2bas  19384  pmtrsn  19511  odf  19529  efgsfo  19731  efgrelexlemb  19742  isabli  19788  rngmgpf  20134  mgpf  20225  prdscrngd  20295  xrsmgmdifsgrp  21394  xrs1cmn  21397  cnmgpid  21420  zringnzr  21444  zringunit  21450  zringlpir  21451  zringndrg  21452  pzriprnglem5  21469  pzriprnglem7  21471  pzriprnglem9  21473  pzriprnglem13  21477  zzngim  21544  cnmsgngrp  21569  psgninv  21572  zrhpsgnmhm  21574  retos  21608  refld  21609  rzgrp  21613  pjpm  21700  fntopon  22912  istpsi  22930  cmpfi  23398  indisconn  23408  kqf  23737  fbssfi  23827  zfbas  23886  ptcmplem2  24043  prdstmdd  24114  tsmsfbas  24118  ismeti  24317  prdsxmslem2  24524  cnfldms  24778  cnnrg  24783  tgqioo  24802  xrtgioo  24808  recld2  24816  xrge0gsumle  24835  xrge0tsms  24836  addcnlem  24866  divcnOLD  24870  divcn  24872  abscncf  24907  recncf  24908  imcncf  24909  cjcncf  24910  icopnfhmeo  24954  xrhmeo  24957  cnllycmp  24968  isclmi0  25111  iscvsi  25142  cnstrcvs  25154  cncms  25369  ovolf  25497  ovolre  25540  opnmblALT  25618  dveflem  25997  mdegxrf  26090  iaa  26348  ulmdm  26417  dvradcnv  26445  reeff1o  26472  reefiso  26473  reefgim  26475  recosf1o  26557  efifo  26569  logcn  26669  cxpcn3  26771  resqrtcn  26772  logb1  26792  logbmpt  26811  2logb9irrALT  26821  sqrt2cxp2logb9e3  26822  ressatans  26957  lgamcvg2  27078  lgam1  27087  gam1  27088  efnnfsumcl  27126  efchtdvds  27182  ppiub  27228  lgslem2  27322  lgsfcl2  27327  lgsne0  27359  2lgslem1b  27416  padicabvf  27655  bdayfo  27702  scutf  27837  madef  27875  scutfo  27922  addsf  27991  addsfo  27992  negsf  28056  negsfo  28057  negsf1o  28058  subsfo  28067  0ons  28245  1ons  28246  dfn0s2  28299  1nns  28313  0reno  28343  istrkg3ld  28383  axlowdimlem16  28886  upgrbi  29024  umgrbi  29032  lfuhgr1v0e  29185  cusgr0  29357  wlk2v2elem2  30084  upgr4cycl4dv4e  30113  konigsberglem4  30183  frgr0  30193  ex-pss  30356  ex-fl  30375  ex-mod  30377  isgrpoi  30426  grporn  30449  isabloi  30479  smcnlem  30625  lnocoi  30685  cncph  30747  cnbn  30797  cnchl  30844  norm3adifii  31076  hhph  31106  hhhl  31132  hlim0  31163  hlimf  31165  helch  31171  hsn0elch  31176  hhssabloilem  31189  hhssnv  31192  hhshsslem2  31196  hhssbnOLD  31207  shscli  31245  shintcli  31257  chintcli  31259  shsval2i  31315  pjhthlem2  31320  lejdii  31466  nonbooli  31579  pjrni  31630  pjfoi  31631  pjfi  31632  pjmf1  31644  df0op2  31680  idunop  31906  0cnop  31907  0cnfn  31908  idcnop  31909  idhmop  31910  0hmop  31911  0lnfn  31913  0bdop  31921  lnophsi  31929  lnopcoi  31931  lnopunii  31940  lnophmi  31946  nmcopex  31957  nmcoplb  31958  nmcfnex  31981  nmcfnlb  31982  imaelshi  31986  nlelshi  31988  nlelchi  31989  riesz4i  31991  riesz4  31992  riesz1  31993  cnlnadjlem6  32000  cnlnadjlem9  32003  cnlnadjeui  32005  cnlnadjeu  32006  nmopadji  32018  bdophsi  32024  bdopcoi  32026  nmopcoadji  32029  pjhmopi  32074  pjbdlni  32077  hmopidmchi  32079  mdslj1i  32247  rinvf1o  32545  nnindf  32721  rpdp2cl  32744  dp2ltc  32749  dpmul4  32776  s3clhash  32812  xrstos  32891  xrsclat  32892  xrge0tsmsd  32928  xrge0omnd  32948  cnfldfld  33222  reofld  33223  nn0archi  33226  zringidom  33430  zringfrac  33433  ccfldextrr  33541  ccfldsrarelvec  33561  ccfldextdgrr  33562  2sqr3minply  33618  xrge0iifmhm  33765  xrge0pluscn  33766  cnzh  33796  rezh  33797  qqhval2lem  33807  esum0  33893  esumcst  33907  esumpcvgval  33922  esumcvg  33930  dmvlsiga  33973  measdivcstALTV  34069  eulerpartlemt  34216  coinfliprv  34327  ballotlem2  34333  signswmnd  34414  logdivsqrle  34507  hgt750lem  34508  bnj906  34786  indispconn  35073  cnllysconn  35084  rellysconn  35090  msrf  35381  brbigcup  35733  fobigcup  35735  brsingle  35752  fnsingle  35754  brimage  35761  funimage  35763  fnimage  35764  imageval  35765  brcart  35767  brapply  35773  brcup  35774  brcap  35775  funpartfun  35778  brub  35789  mpomulnzcnf  36022  onsucconni  36160  onsucsuccmpi  36166  dnicn  36206  bj-wnfnf  36455  bj-nnfv  36470  bj-nnfa1  36475  bj-nnfe1  36476  bj-rabtr  36647  taupilem2  37040  taupi  37041  f1omptsnlem  37054  icoreresf  37070  relowlpssretop  37082  finxpreclem3  37111  matunitlindf  37330  mblfinlem2  37370  areacirc  37425  0totbnd  37485  heiborlem6  37528  refrelid  38231  idsymrel  38270  trrelressn  38292  refrelsredund4  38341  refrelredund4  38344  disjALTV0  38463  disjALTVid  38464  antisymrelressn  38473  isolatiN  38925  isomliN  38948  ishlatiN  39064  mzpclall  42419  jm2.20nn  42690  dfacbasgrp  42804  dgraaf  42843  onexoegt  42944  omnord1  43006  oege2  43008  oenord1  43017  cantnftermord  43021  cantnf2  43026  omabs2  43033  omcl2  43034  ifpim3  43198  ifpim4  43200  ifpbi1b  43205  eu0  43222  omiscard  43245  iso0  44016  dvsid  44040  halffl  44945  resincncf  45530  0cnf  45532  iblempty  45620  dirkeritg  45757  fourierdlem62  45823  fourierdlem76  45837  fourierdlem103  45864  etransclem18  45907  etransclem46  45935  abnotbtaxb  46564  dfaiota3  46739  sprsymrelf1  47102  fmtnof1  47141  fmtno4prm  47181  prmdvdsfmtnof1  47193  31prm  47203  requad01  47227  0evenALTV  47294  1oddALTV  47296  2evenALTV  47298  6even  47317  8even  47319  6gbe  47377  7gbow  47378  8gbe  47379  9gbo  47380  11gbo  47381  uspgrsprf1  47558  1odd  47582  nnsgrp  47588  0even  47648  2even  47650  2zrngamgm  47656  2zrngasgrp  47657  2zrngamnd  47658  2zrngagrp  47660  2zrngmsgrp  47664  zlmodzxzldeplem3  47919  lvecpsslmod  47924  ldepsnlinc  47925  blennngt2o2  48014  blennn0e2  48016  ackval42  48118  rrx2xpref1o  48140  rrx2plordisom  48145  sepfsepc  48295  setrec2lem2  48474  aacllem  48583