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  3952  elini  4150  dtruALT2  5309  exexneq  5378  opnzi  5417  so0  5565  we0  5614  difxp  6113  ord0  6361  dfiota4  6474  funi  6514  funcnvsn  6532  idfn  6610  fn0  6613  f0  6705  fconst  6710  f10  6797  f1o0  6801  f1oi  6802  f1osn  6804  isoid  7266  porpss  7663  epweon  7711  epweonALT  7712  ordon  7713  omssnlim  7814  peano1  7822  fo1st  7944  fo2nd  7945  soseq  8092  iordsmo  8280  tfrlem7  8305  tfr1  8319  frfnom  8357  seqomlem2  8373  oawordeulem  8472  1onn  8558  2onn  8560  naddf  8599  mapsnf1o2  8821  canth2  9047  1sdom2  9137  unfilem2  9195  cantnfvalf  9561  cnfcom3clem  9601  ssttrcl  9611  tc2  9638  r111  9671  rankf  9690  cardf2  9839  harcard  9874  r0weon  9906  infxpenc  9912  infxpenc2lem1  9913  alephon  9963  alephf1  9979  alephiso  9992  alephsmo  9996  alephf1ALT  9997  alephfplem4  10001  ackbij1lem17  10129  ackbij1  10131  ackbij2  10136  fin1a2lem2  10295  fin1a2lem4  10297  axcc2lem  10330  iunfo  10433  smobeth  10480  0tsk  10649  1pi  10777  nqerf  10824  axaddf  11039  axmulf  11040  axicn  11044  mpoaddf  11103  mpomulf  11104  mulnzcnf  11766  negiso  12105  dfnn2  12141  nnind  12146  0z  12482  dfuzi  12567  cnref1o  12886  elrpii  12896  0e0icopnf  13361  0e0iccpnf  13362  fldiv4p1lem1div2  13739  om2uzf1oi  13860  om2uzisoi  13861  uzrdgfni  13865  expcl2lem  13980  expclzlem  13990  expge0  14005  expge1  14006  faclbnd4lem1  14200  hashkf  14239  wwlktovf1  14864  sqrtf  15271  fclim  15460  fprodn0f  15898  eff2  16008  reeff1  16029  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  sin01gt0  16099  egt2lt3  16115  qnnen  16122  ruc  16152  halfleoddlt  16273  divalglem2  16306  divalglem9  16312  bitsf1  16357  sadaddlem  16377  2prm  16603  3prm  16605  1arith  16839  prmlem1a  17018  setsnid  17119  xpsff1o  17471  dmaf  17956  cdaf  17957  coapm  17978  0pos  18227  isposi  18229  letsr  18499  sgrp0b  18602  frmdplusg  18728  efmndsgrp  18760  smndex1sgrp  18782  smndex1mnd  18784  symg2bas  19272  pmtrsn  19398  odf  19416  efgsfo  19618  efgrelexlemb  19629  isabli  19675  rngmgpf  20042  mgpf  20133  prdscrngd  20207  xrsmgmdifsgrp  21315  cnmgpid  21336  xrs1cmn  21349  xrge0omnd  21352  zringnzr  21367  zringunit  21373  zringlpir  21374  zringndrg  21375  pzriprnglem5  21392  pzriprnglem7  21394  pzriprnglem9  21396  pzriprnglem13  21400  zzngim  21459  cnmsgngrp  21486  psgninv  21489  zrhpsgnmhm  21491  retos  21525  refld  21526  rzgrp  21530  pjpm  21615  fntopon  22809  istpsi  22827  cmpfi  23293  indisconn  23303  kqf  23632  fbssfi  23722  zfbas  23781  ptcmplem2  23938  prdstmdd  24009  tsmsfbas  24013  ismeti  24211  prdsxmslem2  24415  cnfldms  24661  cnnrg  24666  tgqioo  24686  xrtgioo  24693  recld2  24701  xrge0gsumle  24720  xrge0tsms  24721  addcnlem  24751  divcnOLD  24755  divcn  24757  abscncf  24792  recncf  24793  imcncf  24794  cjcncf  24795  icopnfhmeo  24839  xrhmeo  24842  cnllycmp  24853  isclmi0  24996  iscvsi  25027  cnstrcvs  25039  cncms  25253  ovolf  25381  ovolre  25424  opnmblALT  25502  dveflem  25881  mdegxrf  25971  iaa  26231  ulmdm  26300  dvradcnv  26328  reeff1o  26355  reefiso  26356  reefgim  26358  recosf1o  26442  efifo  26454  logcn  26554  cxpcn3  26656  resqrtcn  26657  logb1  26677  logbmpt  26696  2logb9irrALT  26706  sqrt2cxp2logb9e3  26707  ressatans  26842  lgamcvg2  26963  lgam1  26972  gam1  26973  efnnfsumcl  27011  efchtdvds  27067  ppiub  27113  lgslem2  27207  lgsfcl2  27212  lgsne0  27244  2lgslem1b  27301  padicabvf  27540  bdayfo  27587  scutf  27723  madef  27766  scutfo  27819  addsf  27894  addsfo  27895  negsf  27963  negsfo  27964  negsf1o  27965  subsfo  27974  0ons  28162  1ons  28163  onsiso  28174  dfn0s2  28229  1nns  28246  bdayn0sf1o  28264  zsoring  28301  twocut  28315  0reno  28366  istrkg3ld  28406  axlowdimlem16  28902  upgrbi  29038  umgrbi  29046  lfuhgr1v0e  29199  cusgr0  29371  wlk2v2elem2  30100  upgr4cycl4dv4e  30129  konigsberglem4  30199  frgr0  30209  ex-pss  30372  ex-fl  30391  ex-mod  30393  isgrpoi  30442  grporn  30465  isabloi  30495  smcnlem  30641  lnocoi  30701  cncph  30763  cnbn  30813  cnchl  30860  norm3adifii  31092  hhph  31122  hhhl  31148  hlim0  31179  hlimf  31181  helch  31187  hsn0elch  31192  hhssabloilem  31205  hhssnv  31208  hhshsslem2  31212  hhssbnOLD  31223  shscli  31261  shintcli  31273  chintcli  31275  shsval2i  31331  pjhthlem2  31336  lejdii  31482  nonbooli  31595  pjrni  31646  pjfoi  31647  pjfi  31648  pjmf1  31660  df0op2  31696  idunop  31922  0cnop  31923  0cnfn  31924  idcnop  31925  idhmop  31926  0hmop  31927  0lnfn  31929  0bdop  31937  lnophsi  31945  lnopcoi  31947  lnopunii  31956  lnophmi  31962  nmcopex  31973  nmcoplb  31974  nmcfnex  31997  nmcfnlb  31998  imaelshi  32002  nlelshi  32004  nlelchi  32005  riesz4i  32007  riesz4  32008  riesz1  32009  cnlnadjlem6  32016  cnlnadjlem9  32019  cnlnadjeui  32021  cnlnadjeu  32022  nmopadji  32034  bdophsi  32040  bdopcoi  32042  nmopcoadji  32045  pjhmopi  32090  pjbdlni  32093  hmopidmchi  32095  mdslj1i  32263  rinvf1o  32574  nnindf  32765  rpdp2cl  32823  dp2ltc  32828  dpmul4  32855  s3clhash  32890  xrstos  32965  xrsclat  32966  xrge0tsmsd  33016  qfld  33237  cnfldfld  33281  reofld  33282  nn0archi  33285  zringidom  33489  zringfrac  33492  ccfldextrr  33619  ccfldsrarelvec  33644  ccfldextdgrr  33645  2sqr3minply  33753  xrge0iifmhm  33912  xrge0pluscn  33913  cnzh  33941  rezh  33942  qqhval2lem  33954  esum0  34022  esumcst  34036  esumpcvgval  34051  esumcvg  34059  dmvlsiga  34102  measdivcstALTV  34198  eulerpartlemt  34345  coinfliprv  34457  ballotlem2  34463  signswmnd  34531  logdivsqrle  34624  hgt750lem  34625  bnj906  34903  fineqvnttrclse  35083  indispconn  35217  cnllysconn  35228  rellysconn  35234  msrf  35525  brbigcup  35882  fobigcup  35884  brsingle  35901  fnsingle  35903  brimage  35910  funimage  35912  fnimage  35913  imageval  35914  brcart  35916  brapply  35922  brcup  35923  brcap  35924  funpartfun  35927  brub  35938  mpomulnzcnf  36283  onsucconni  36421  onsucsuccmpi  36427  dnicn  36476  bj-wnfnf  36723  bj-nnfv  36738  bj-nnfa1  36743  bj-nnfe1  36744  bj-rabtr  36914  taupilem2  37306  taupi  37307  f1omptsnlem  37320  icoreresf  37336  relowlpssretop  37348  finxpreclem3  37377  matunitlindf  37608  mblfinlem2  37648  areacirc  37703  0totbnd  37763  heiborlem6  37806  refrelid  38509  idsymrel  38548  trrelressn  38570  refrelsredund4  38619  refrelredund4  38622  disjALTV0  38742  disjALTVid  38743  antisymrelressn  38752  isolatiN  39205  isomliN  39228  ishlatiN  39344  mzpclall  42710  jm2.20nn  42980  dfacbasgrp  43091  dgraaf  43130  onexoegt  43227  omnord1  43288  oege2  43290  oenord1  43299  cantnftermord  43303  cantnf2  43308  omabs2  43315  omcl2  43316  ifpim3  43479  ifpim4  43481  ifpbi1b  43486  eu0  43503  omiscard  43526  iso0  44290  dvsid  44314  rankrelp  44944  halffl  45288  resincncf  45866  0cnf  45868  iblempty  45956  dirkeritg  46093  fourierdlem62  46159  fourierdlem76  46173  fourierdlem103  46200  etransclem18  46243  etransclem46  46271  abnotbtaxb  46909  dfaiota3  47086  ceilhalf1  47328  sprsymrelf1  47490  fmtnof1  47529  fmtno4prm  47569  prmdvdsfmtnof1  47581  31prm  47591  requad01  47615  0evenALTV  47682  1oddALTV  47684  2evenALTV  47686  6even  47705  8even  47707  6gbe  47765  7gbow  47766  8gbe  47767  9gbo  47768  11gbo  47769  usgrexmpl1lem  48015  usgrexmpl2lem  48020  usgrexmpl2trifr  48031  gpg5grlim  48087  gpg5grlic  48088  uspgrsprf1  48141  1odd  48165  nnsgrp  48171  0even  48231  2even  48233  2zrngamgm  48239  2zrngasgrp  48240  2zrngamnd  48241  2zrngagrp  48243  2zrngmsgrp  48247  zlmodzxzldeplem3  48497  lvecpsslmod  48502  ldepsnlinc  48503  blennngt2o2  48587  blennn0e2  48589  ackval42  48691  rrx2xpref1o  48713  rrx2plordisom  48718  slotresfo  48893  sepfsepc  48922  basresposfo  48972  oppff1  49143  setcsnterm  49485  setc1onsubc  49597  setrec2lem2  49689  aacllem  49796