Theorem mpbir2an 712

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  3pm3.2i  1341  euequ  2597  eqssi  3938  elini  4139  dtruALT2  5312  exexneq  5387  opnzi  5427  so0  5577  we0  5626  difxp  6128  ord0  6377  dfiota4  6490  funi  6530  funcnvsn  6548  idfn  6626  fn0  6629  f0  6721  fconst  6726  f10  6813  f1o0  6817  f1oiOLD  6819  f1osn  6821  isoid  7284  porpss  7681  epweon  7729  epweonALT  7730  ordon  7731  omssnlim  7832  peano1  7840  fo1st  7962  fo2nd  7963  soseq  8109  iordsmo  8297  tfrlem7  8322  tfr1  8336  frfnom  8374  seqomlem2  8390  oawordeulem  8489  1onn  8576  2onn  8578  naddf  8617  mapsnf1o2  8842  canth2  9068  1sdom2  9158  unfilem2  9216  cantnfvalf  9586  cnfcom3clem  9626  ssttrcl  9636  tc2  9661  r111  9699  rankf  9718  cardf2  9867  harcard  9902  r0weon  9934  infxpenc  9940  infxpenc2lem1  9941  alephon  9991  alephf1  10007  alephiso  10020  alephsmo  10024  alephf1ALT  10025  alephfplem4  10029  ackbij1lem17  10157  ackbij1  10159  ackbij2  10164  fin1a2lem2  10323  fin1a2lem4  10325  axcc2lem  10358  iunfo  10461  smobeth  10509  0tsk  10678  1pi  10806  nqerf  10853  axaddf  11068  axmulf  11069  axicn  11073  mpoaddf  11132  mpomulf  11133  mulnzcnf  11796  negiso  12136  dfnn2  12187  nnind  12192  0z  12535  dfuzi  12620  cnref1o  12935  elrpii  12945  0e0icopnf  13411  0e0iccpnf  13412  fldiv4p1lem1div2  13794  om2uzf1oi  13915  om2uzisoi  13916  uzrdgfni  13920  expcl2lem  14035  expclzlem  14045  expge0  14060  expge1  14061  faclbnd4lem1  14255  hashkf  14294  wwlktovf1  14919  sqrtf  15326  fclim  15515  fprodn0f  15956  eff2  16066  reeff1  16087  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  egt2lt3  16173  qnnen  16180  ruc  16210  halfleoddlt  16331  divalglem2  16364  divalglem9  16370  bitsf1  16415  sadaddlem  16435  2prm  16661  3prm  16663  1arith  16898  prmlem1a  17077  setsnid  17178  xpsff1o  17531  dmaf  18016  cdaf  18017  coapm  18038  0pos  18287  isposi  18289  letsr  18559  ex-chn1  18603  ex-chn2  18604  sgrp0b  18696  frmdplusg  18822  efmndsgrp  18854  smndex1sgrp  18879  smndex1mnd  18881  symg2bas  19368  pmtrsn  19494  odf  19512  efgsfo  19714  efgrelexlemb  19725  isabli  19771  rngmgpf  20138  mgpf  20229  prdscrngd  20301  xrsmgmdifsgrp  21389  cnmgpid  21409  xrs1cmn  21422  xrge0omnd  21425  zringnzr  21440  zringunit  21446  zringlpir  21447  zringndrg  21448  pzriprnglem5  21465  pzriprnglem7  21467  pzriprnglem9  21469  pzriprnglem13  21473  zzngim  21532  cnmsgngrp  21559  psgninv  21562  zrhpsgnmhm  21564  retos  21598  refld  21599  rzgrp  21603  pjpm  21688  fntopon  22889  istpsi  22907  cmpfi  23373  indisconn  23383  kqf  23712  fbssfi  23802  zfbas  23861  ptcmplem2  24018  prdstmdd  24089  tsmsfbas  24093  ismeti  24290  prdsxmslem2  24494  cnfldms  24740  cnnrg  24745  tgqioo  24765  xrtgioo  24772  recld2  24780  xrge0gsumle  24799  xrge0tsms  24800  addcnlem  24830  divcn  24835  abscncf  24868  recncf  24869  imcncf  24870  cjcncf  24871  icopnfhmeo  24910  xrhmeo  24913  cnllycmp  24923  isclmi0  25065  iscvsi  25096  cnstrcvs  25108  cncms  25322  ovolf  25449  ovolre  25492  opnmblALT  25570  dveflem  25946  mdegxrf  26033  iaa  26291  ulmdm  26358  dvradcnv  26386  reeff1o  26412  reefiso  26413  reefgim  26415  recosf1o  26499  efifo  26511  logcn  26611  cxpcn3  26712  resqrtcn  26713  logb1  26733  logbmpt  26752  2logb9irrALT  26762  sqrt2cxp2logb9e3  26763  ressatans  26898  lgamcvg2  27018  lgam1  27027  gam1  27028  efnnfsumcl  27066  efchtdvds  27122  ppiub  27167  lgslem2  27261  lgsfcl2  27266  lgsne0  27298  2lgslem1b  27355  padicabvf  27594  bdayfo  27641  cutsf  27784  madef  27828  cutsfo  27897  addsf  27974  addsfo  27975  negsf  28044  negsfo  28045  negsf1o  28046  subsfo  28057  0ons  28248  1ons  28249  oniso  28263  dfn0s2  28324  1nns  28341  bdayn0sf1o  28362  zsoring  28401  twocut  28415  0reno  28488  1reno  28489  istrkg3ld  28529  axlowdimlem16  29026  upgrbi  29162  umgrbi  29170  lfuhgr1v0e  29323  cusgr0  29495  wlk2v2elem2  30226  upgr4cycl4dv4e  30255  konigsberglem4  30325  frgr0  30335  ex-pss  30498  ex-fl  30517  ex-mod  30519  isgrpoi  30569  grporn  30592  isabloi  30622  smcnlem  30768  lnocoi  30828  cncph  30890  cnbn  30940  cnchl  30987  norm3adifii  31219  hhph  31249  hhhl  31275  hlim0  31306  hlimf  31308  helch  31314  hsn0elch  31319  hhssabloilem  31332  hhssnv  31335  hhshsslem2  31339  hhssbnOLD  31350  shscli  31388  shintcli  31400  chintcli  31402  shsval2i  31458  pjhthlem2  31463  lejdii  31609  nonbooli  31722  pjrni  31773  pjfoi  31774  pjfi  31775  pjmf1  31787  df0op2  31823  idunop  32049  0cnop  32050  0cnfn  32051  idcnop  32052  idhmop  32053  0hmop  32054  0lnfn  32056  0bdop  32064  lnophsi  32072  lnopcoi  32074  lnopunii  32083  lnophmi  32089  nmcopex  32100  nmcoplb  32101  nmcfnex  32124  nmcfnlb  32125  imaelshi  32129  nlelshi  32131  nlelchi  32132  riesz4i  32134  riesz4  32135  riesz1  32136  cnlnadjlem6  32143  cnlnadjlem9  32146  cnlnadjeui  32148  cnlnadjeu  32149  nmopadji  32161  bdophsi  32167  bdopcoi  32169  nmopcoadji  32172  pjhmopi  32217  pjbdlni  32220  hmopidmchi  32222  mdslj1i  32390  rinvf1o  32703  nnindf  32893  rpdp2cl  32941  dp2ltc  32946  dpmul4  32973  s3clhash  33008  xrstos  33070  xrsclat  33071  xrge0tsmsd  33134  qfld  33358  cnfldfld  33402  reofld  33403  nn0archi  33407  zringidom  33611  zringfrac  33614  ccfldextrr  33790  ccfldsrarelvec  33815  ccfldextdgrr  33816  2sqr3minply  33924  xrge0iifmhm  34083  xrge0pluscn  34084  cnzh  34112  rezh  34113  qqhval2lem  34125  esum0  34193  esumcst  34207  esumpcvgval  34222  esumcvg  34230  dmvlsiga  34273  measdivcstALTV  34369  eulerpartlemt  34515  coinfliprv  34627  ballotlem2  34633  signswmnd  34701  logdivsqrle  34794  hgt750lem  34795  bnj906  35072  xoromon  35232  fineqvnttrclse  35268  indispconn  35416  cnllysconn  35427  rellysconn  35433  msrf  35724  brbigcup  36078  fobigcup  36080  brsingle  36097  fnsingle  36099  brimage  36106  funimage  36108  fnimage  36109  imageval  36110  brcart  36112  brapply  36118  brcup  36119  brcap  36120  funpartfun  36125  brub  36136  mpomulnzcnf  36481  onsucconni  36619  onsucsuccmpi  36625  dnicn  36752  bj-nnfv  37065  bj-wnfnf  37080  bj-nnfa1  37081  bj-nnfe1  37082  bj-rabtr  37237  bj-axreprepsep  37382  taupilem2  37636  taupi  37637  f1omptsnlem  37652  icoreresf  37668  relowlpssretop  37680  finxpreclem3  37709  matunitlindf  37939  mblfinlem2  37979  areacirc  38034  0totbnd  38094  heiborlem6  38137  dfsucmap3  38784  refrelid  38923  idsymrel  38966  trrelressn  38988  refrelsredund4  39037  refrelredund4  39040  disjALTV0  39175  disjALTVid  39176  antisymrelressn  39188  isolatiN  39662  isomliN  39685  ishlatiN  39801  mzpclall  43159  jm2.20nn  43425  dfacbasgrp  43536  dgraaf  43575  onexoegt  43672  omnord1  43733  oege2  43735  oenord1  43744  cantnftermord  43748  cantnf2  43753  omabs2  43760  omcl2  43761  ifpim3  43923  ifpim4  43925  ifpbi1b  43930  eu0  43947  omiscard  43970  iso0  44734  dvsid  44758  rankrelp  45387  halffl  45729  resincncf  46303  0cnf  46305  iblempty  46393  dirkeritg  46530  fourierdlem62  46596  fourierdlem76  46610  fourierdlem103  46637  etransclem18  46680  etransclem46  46708  abnotbtaxb  47363  dfaiota3  47540  ceilhalf1  47786  sprsymrelf1  47956  fmtnof1  47998  fmtno4prm  48038  prmdvdsfmtnof1  48050  31prm  48060  requad01  48097  0evenALTV  48164  1oddALTV  48166  2evenALTV  48168  6even  48187  8even  48189  6gbe  48247  7gbow  48248  8gbe  48249  9gbo  48250  11gbo  48251  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2trifr  48513  gpg5grlim  48569  gpg5grlic  48570  uspgrsprf1  48623  1odd  48647  nnsgrp  48653  0even  48713  2even  48715  2zrngamgm  48721  2zrngasgrp  48722  2zrngamnd  48723  2zrngagrp  48725  2zrngmsgrp  48729  zlmodzxzldeplem3  48978  lvecpsslmod  48983  ldepsnlinc  48984  blennngt2o2  49068  blennn0e2  49070  ackval42  49172  rrx2xpref1o  49194  rrx2plordisom  49199  slotresfo  49374  sepfsepc  49403  basresposfo  49453  oppff1  49623  setcsnterm  49965  setc1onsubc  50077  setrec2lem2  50169  aacllem  50276