Theorem mpbir2an 711

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 709	. 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  1340  euequ  2590  eqssi  3954  elini  4152  dtruALT2  5312  exexneq  5381  dtruOLD  5388  opnzi  5421  so0  5569  we0  5618  difxp  6117  ord0  6365  dfiota4  6478  funi  6518  funcnvsn  6536  idfn  6614  fn0  6617  f0  6709  fconst  6714  f10  6801  f1o0  6805  f1oi  6806  f1osn  6808  isoid  7270  porpss  7667  epweon  7715  epweonALT  7716  ordon  7717  omssnlim  7821  peano1  7829  fo1st  7951  fo2nd  7952  soseq  8099  iordsmo  8287  tfrlem7  8312  tfr1  8326  frfnom  8364  seqomlem2  8380  oawordeulem  8479  1onn  8565  2onn  8567  naddf  8606  mapsnf1o2  8828  canth2  9054  1sdom2  9147  unfilem2  9213  cantnfvalf  9580  cnfcom3clem  9620  ssttrcl  9630  tc2  9657  r111  9690  rankf  9709  cardf2  9858  harcard  9893  r0weon  9925  infxpenc  9931  infxpenc2lem1  9932  alephon  9982  alephf1  9998  alephiso  10011  alephsmo  10015  alephf1ALT  10016  alephfplem4  10020  ackbij1lem17  10148  ackbij1  10150  ackbij2  10155  fin1a2lem2  10314  fin1a2lem4  10316  axcc2lem  10349  iunfo  10452  smobeth  10499  0tsk  10668  1pi  10796  nqerf  10843  axaddf  11058  axmulf  11059  axicn  11063  mpoaddf  11122  mpomulf  11123  mulnzcnf  11784  negiso  12123  dfnn2  12159  nnind  12164  0z  12500  dfuzi  12585  cnref1o  12904  elrpii  12914  0e0icopnf  13379  0e0iccpnf  13380  fldiv4p1lem1div2  13757  om2uzf1oi  13878  om2uzisoi  13879  uzrdgfni  13883  expcl2lem  13998  expclzlem  14008  expge0  14023  expge1  14024  faclbnd4lem1  14218  hashkf  14257  wwlktovf1  14882  sqrtf  15289  fclim  15478  fprodn0f  15916  eff2  16026  reeff1  16047  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  sin01gt0  16117  egt2lt3  16133  qnnen  16140  ruc  16170  halfleoddlt  16291  divalglem2  16324  divalglem9  16330  bitsf1  16375  sadaddlem  16395  2prm  16621  3prm  16623  1arith  16857  prmlem1a  17036  setsnid  17137  xpsff1o  17489  dmaf  17974  cdaf  17975  coapm  17996  0pos  18245  isposi  18247  letsr  18517  sgrp0b  18620  frmdplusg  18746  efmndsgrp  18778  smndex1sgrp  18800  smndex1mnd  18802  symg2bas  19290  pmtrsn  19416  odf  19434  efgsfo  19636  efgrelexlemb  19647  isabli  19693  rngmgpf  20060  mgpf  20151  prdscrngd  20225  xrsmgmdifsgrp  21333  cnmgpid  21354  xrs1cmn  21367  xrge0omnd  21370  zringnzr  21385  zringunit  21391  zringlpir  21392  zringndrg  21393  pzriprnglem5  21410  pzriprnglem7  21412  pzriprnglem9  21414  pzriprnglem13  21418  zzngim  21477  cnmsgngrp  21504  psgninv  21507  zrhpsgnmhm  21509  retos  21543  refld  21544  rzgrp  21548  pjpm  21633  fntopon  22827  istpsi  22845  cmpfi  23311  indisconn  23321  kqf  23650  fbssfi  23740  zfbas  23799  ptcmplem2  23956  prdstmdd  24027  tsmsfbas  24031  ismeti  24229  prdsxmslem2  24433  cnfldms  24679  cnnrg  24684  tgqioo  24704  xrtgioo  24711  recld2  24719  xrge0gsumle  24738  xrge0tsms  24739  addcnlem  24769  divcnOLD  24773  divcn  24775  abscncf  24810  recncf  24811  imcncf  24812  cjcncf  24813  icopnfhmeo  24857  xrhmeo  24860  cnllycmp  24871  isclmi0  25014  iscvsi  25045  cnstrcvs  25057  cncms  25271  ovolf  25399  ovolre  25442  opnmblALT  25520  dveflem  25899  mdegxrf  25989  iaa  26249  ulmdm  26318  dvradcnv  26346  reeff1o  26373  reefiso  26374  reefgim  26376  recosf1o  26460  efifo  26472  logcn  26572  cxpcn3  26674  resqrtcn  26675  logb1  26695  logbmpt  26714  2logb9irrALT  26724  sqrt2cxp2logb9e3  26725  ressatans  26860  lgamcvg2  26981  lgam1  26990  gam1  26991  efnnfsumcl  27029  efchtdvds  27085  ppiub  27131  lgslem2  27225  lgsfcl2  27230  lgsne0  27262  2lgslem1b  27319  padicabvf  27558  bdayfo  27605  scutf  27741  madef  27784  scutfo  27837  addsf  27912  addsfo  27913  negsf  27981  negsfo  27982  negsf1o  27983  subsfo  27992  0ons  28180  1ons  28181  onsiso  28192  dfn0s2  28247  1nns  28264  bdayn0sf1o  28282  zsoring  28319  twocut  28333  0reno  28384  istrkg3ld  28424  axlowdimlem16  28920  upgrbi  29056  umgrbi  29064  lfuhgr1v0e  29217  cusgr0  29389  wlk2v2elem2  30118  upgr4cycl4dv4e  30147  konigsberglem4  30217  frgr0  30227  ex-pss  30390  ex-fl  30409  ex-mod  30411  isgrpoi  30460  grporn  30483  isabloi  30513  smcnlem  30659  lnocoi  30719  cncph  30781  cnbn  30831  cnchl  30878  norm3adifii  31110  hhph  31140  hhhl  31166  hlim0  31197  hlimf  31199  helch  31205  hsn0elch  31210  hhssabloilem  31223  hhssnv  31226  hhshsslem2  31230  hhssbnOLD  31241  shscli  31279  shintcli  31291  chintcli  31293  shsval2i  31349  pjhthlem2  31354  lejdii  31500  nonbooli  31613  pjrni  31664  pjfoi  31665  pjfi  31666  pjmf1  31678  df0op2  31714  idunop  31940  0cnop  31941  0cnfn  31942  idcnop  31943  idhmop  31944  0hmop  31945  0lnfn  31947  0bdop  31955  lnophsi  31963  lnopcoi  31965  lnopunii  31974  lnophmi  31980  nmcopex  31991  nmcoplb  31992  nmcfnex  32015  nmcfnlb  32016  imaelshi  32020  nlelshi  32022  nlelchi  32023  riesz4i  32025  riesz4  32026  riesz1  32027  cnlnadjlem6  32034  cnlnadjlem9  32037  cnlnadjeui  32039  cnlnadjeu  32040  nmopadji  32052  bdophsi  32058  bdopcoi  32060  nmopcoadji  32063  pjhmopi  32108  pjbdlni  32111  hmopidmchi  32113  mdslj1i  32281  rinvf1o  32587  nnindf  32777  rpdp2cl  32835  dp2ltc  32840  dpmul4  32867  s3clhash  32902  xrstos  32977  xrsclat  32978  xrge0tsmsd  33028  qfld  33246  cnfldfld  33290  reofld  33291  nn0archi  33294  zringidom  33498  zringfrac  33501  ccfldextrr  33618  ccfldsrarelvec  33642  ccfldextdgrr  33643  2sqr3minply  33746  xrge0iifmhm  33905  xrge0pluscn  33906  cnzh  33934  rezh  33935  qqhval2lem  33947  esum0  34015  esumcst  34029  esumpcvgval  34044  esumcvg  34052  dmvlsiga  34095  measdivcstALTV  34191  eulerpartlemt  34338  coinfliprv  34450  ballotlem2  34456  signswmnd  34524  logdivsqrle  34617  hgt750lem  34618  bnj906  34896  indispconn  35206  cnllysconn  35217  rellysconn  35223  msrf  35514  brbigcup  35871  fobigcup  35873  brsingle  35890  fnsingle  35892  brimage  35899  funimage  35901  fnimage  35902  imageval  35903  brcart  35905  brapply  35911  brcup  35912  brcap  35913  funpartfun  35916  brub  35927  mpomulnzcnf  36272  onsucconni  36410  onsucsuccmpi  36416  dnicn  36465  bj-wnfnf  36712  bj-nnfv  36727  bj-nnfa1  36732  bj-nnfe1  36733  bj-rabtr  36903  taupilem2  37295  taupi  37296  f1omptsnlem  37309  icoreresf  37325  relowlpssretop  37337  finxpreclem3  37366  matunitlindf  37597  mblfinlem2  37637  areacirc  37692  0totbnd  37752  heiborlem6  37795  refrelid  38498  idsymrel  38537  trrelressn  38559  refrelsredund4  38608  refrelredund4  38611  disjALTV0  38731  disjALTVid  38732  antisymrelressn  38741  isolatiN  39194  isomliN  39217  ishlatiN  39333  mzpclall  42700  jm2.20nn  42970  dfacbasgrp  43081  dgraaf  43120  onexoegt  43217  omnord1  43278  oege2  43280  oenord1  43289  cantnftermord  43293  cantnf2  43298  omabs2  43305  omcl2  43306  ifpim3  43469  ifpim4  43471  ifpbi1b  43476  eu0  43493  omiscard  43516  iso0  44280  dvsid  44304  rankrelp  44934  halffl  45278  resincncf  45857  0cnf  45859  iblempty  45947  dirkeritg  46084  fourierdlem62  46150  fourierdlem76  46164  fourierdlem103  46191  etransclem18  46234  etransclem46  46262  abnotbtaxb  46900  dfaiota3  47077  ceilhalf1  47319  sprsymrelf1  47481  fmtnof1  47520  fmtno4prm  47560  prmdvdsfmtnof1  47572  31prm  47582  requad01  47606  0evenALTV  47673  1oddALTV  47675  2evenALTV  47677  6even  47696  8even  47698  6gbe  47756  7gbow  47757  8gbe  47758  9gbo  47759  11gbo  47760  usgrexmpl1lem  48006  usgrexmpl2lem  48011  usgrexmpl2trifr  48022  gpg5grlim  48078  gpg5grlic  48079  uspgrsprf1  48132  1odd  48156  nnsgrp  48162  0even  48222  2even  48224  2zrngamgm  48230  2zrngasgrp  48231  2zrngamnd  48232  2zrngagrp  48234  2zrngmsgrp  48238  zlmodzxzldeplem3  48488  lvecpsslmod  48493  ldepsnlinc  48494  blennngt2o2  48578  blennn0e2  48580  ackval42  48682  rrx2xpref1o  48704  rrx2plordisom  48709  slotresfo  48884  sepfsepc  48913  basresposfo  48963  oppff1  49134  setcsnterm  49476  setc1onsubc  49588  setrec2lem2  49680  aacllem  49787