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  2597  eqssi  4000  elini  4199  dtruALT2  5370  exexneq  5439  dtruOLD  5446  opnzi  5479  so0  5630  we0  5680  difxp  6184  ord0  6437  dfiota4  6553  funi  6598  funcnvsn  6616  idfn  6696  fn0  6699  f0  6789  fconst  6794  f10  6881  f1o0  6885  f1oi  6886  f1osn  6888  isoid  7349  porpss  7747  epweon  7795  epweonALT  7796  ordon  7797  omssnlim  7902  peano1  7910  fo1st  8034  fo2nd  8035  soseq  8184  wfrfunOLD  8359  wfr1OLD  8367  iordsmo  8397  tfrlem7  8423  tfr1  8437  frfnom  8475  seqomlem2  8491  oawordeulem  8592  1onn  8678  2onn  8680  naddf  8719  mapsnf1o2  8934  canth2  9170  1sdom2  9276  unfilem2  9344  cantnfvalf  9705  cnfcom3clem  9745  ssttrcl  9755  tc2  9782  r111  9815  rankf  9834  cardf2  9983  harcard  10018  r0weon  10052  infxpenc  10058  infxpenc2lem1  10059  alephon  10109  alephf1  10125  alephiso  10138  alephsmo  10142  alephf1ALT  10143  alephfplem4  10147  ackbij1lem17  10275  ackbij1  10277  ackbij2  10282  fin1a2lem2  10441  fin1a2lem4  10443  axcc2lem  10476  iunfo  10579  smobeth  10626  0tsk  10795  1pi  10923  nqerf  10970  axaddf  11185  axmulf  11186  axicn  11190  mpoaddf  11249  mpomulf  11250  mulnzcnf  11909  negiso  12248  dfnn2  12279  nnind  12284  0z  12624  dfuzi  12709  cnref1o  13027  elrpii  13037  0e0icopnf  13498  0e0iccpnf  13499  fldiv4p1lem1div2  13875  om2uzf1oi  13994  om2uzisoi  13995  uzrdgfni  13999  expcl2lem  14114  expclzlem  14124  expge0  14139  expge1  14140  faclbnd4lem1  14332  hashkf  14371  wwlktovf1  14996  sqrtf  15402  fclim  15589  fprodn0f  16027  eff2  16135  reeff1  16156  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  egt2lt3  16242  qnnen  16249  ruc  16279  halfleoddlt  16399  divalglem2  16432  divalglem9  16438  bitsf1  16483  sadaddlem  16503  2prm  16729  3prm  16731  1arith  16965  prmlem1a  17144  setsnid  17245  setsnidOLD  17246  xpsff1o  17612  dmaf  18094  cdaf  18095  coapm  18116  0pos  18367  isposi  18369  letsr  18638  sgrp0b  18741  frmdplusg  18867  efmndsgrp  18899  smndex1sgrp  18921  smndex1mnd  18923  symg2bas  19410  pmtrsn  19537  odf  19555  efgsfo  19757  efgrelexlemb  19768  isabli  19814  rngmgpf  20154  mgpf  20245  prdscrngd  20319  xrsmgmdifsgrp  21421  xrs1cmn  21424  cnmgpid  21447  zringnzr  21471  zringunit  21477  zringlpir  21478  zringndrg  21479  pzriprnglem5  21496  pzriprnglem7  21498  pzriprnglem9  21500  pzriprnglem13  21504  zzngim  21571  cnmsgngrp  21597  psgninv  21600  zrhpsgnmhm  21602  retos  21636  refld  21637  rzgrp  21641  pjpm  21728  fntopon  22930  istpsi  22948  cmpfi  23416  indisconn  23426  kqf  23755  fbssfi  23845  zfbas  23904  ptcmplem2  24061  prdstmdd  24132  tsmsfbas  24136  ismeti  24335  prdsxmslem2  24542  cnfldms  24796  cnnrg  24801  tgqioo  24821  xrtgioo  24828  recld2  24836  xrge0gsumle  24855  xrge0tsms  24856  addcnlem  24886  divcnOLD  24890  divcn  24892  abscncf  24927  recncf  24928  imcncf  24929  cjcncf  24930  icopnfhmeo  24974  xrhmeo  24977  cnllycmp  24988  isclmi0  25131  iscvsi  25162  cnstrcvs  25174  cncms  25389  ovolf  25517  ovolre  25560  opnmblALT  25638  dveflem  26017  mdegxrf  26107  iaa  26367  ulmdm  26436  dvradcnv  26464  reeff1o  26491  reefiso  26492  reefgim  26494  recosf1o  26577  efifo  26589  logcn  26689  cxpcn3  26791  resqrtcn  26792  logb1  26812  logbmpt  26831  2logb9irrALT  26841  sqrt2cxp2logb9e3  26842  ressatans  26977  lgamcvg2  27098  lgam1  27107  gam1  27108  efnnfsumcl  27146  efchtdvds  27202  ppiub  27248  lgslem2  27342  lgsfcl2  27347  lgsne0  27379  2lgslem1b  27436  padicabvf  27675  bdayfo  27722  scutf  27857  madef  27895  scutfo  27942  addsf  28015  addsfo  28016  negsf  28084  negsfo  28085  negsf1o  28086  subsfo  28095  0ons  28279  1ons  28280  dfn0s2  28336  1nns  28352  nohalf  28407  0reno  28429  istrkg3ld  28469  axlowdimlem16  28972  upgrbi  29110  umgrbi  29118  lfuhgr1v0e  29271  cusgr0  29443  wlk2v2elem2  30175  upgr4cycl4dv4e  30204  konigsberglem4  30274  frgr0  30284  ex-pss  30447  ex-fl  30466  ex-mod  30468  isgrpoi  30517  grporn  30540  isabloi  30570  smcnlem  30716  lnocoi  30776  cncph  30838  cnbn  30888  cnchl  30935  norm3adifii  31167  hhph  31197  hhhl  31223  hlim0  31254  hlimf  31256  helch  31262  hsn0elch  31267  hhssabloilem  31280  hhssnv  31283  hhshsslem2  31287  hhssbnOLD  31298  shscli  31336  shintcli  31348  chintcli  31350  shsval2i  31406  pjhthlem2  31411  lejdii  31557  nonbooli  31670  pjrni  31721  pjfoi  31722  pjfi  31723  pjmf1  31735  df0op2  31771  idunop  31997  0cnop  31998  0cnfn  31999  idcnop  32000  idhmop  32001  0hmop  32002  0lnfn  32004  0bdop  32012  lnophsi  32020  lnopcoi  32022  lnopunii  32031  lnophmi  32037  nmcopex  32048  nmcoplb  32049  nmcfnex  32072  nmcfnlb  32073  imaelshi  32077  nlelshi  32079  nlelchi  32080  riesz4i  32082  riesz4  32083  riesz1  32084  cnlnadjlem6  32091  cnlnadjlem9  32094  cnlnadjeui  32096  cnlnadjeu  32097  nmopadji  32109  bdophsi  32115  bdopcoi  32117  nmopcoadji  32120  pjhmopi  32165  pjbdlni  32168  hmopidmchi  32170  mdslj1i  32338  rinvf1o  32640  nnindf  32821  rpdp2cl  32864  dp2ltc  32869  dpmul4  32896  s3clhash  32932  xrstos  33012  xrsclat  33013  xrge0tsmsd  33065  xrge0omnd  33088  qfld  33300  cnfldfld  33371  reofld  33372  nn0archi  33375  zringidom  33579  zringfrac  33582  ccfldextrr  33699  ccfldsrarelvec  33721  ccfldextdgrr  33722  2sqr3minply  33791  xrge0iifmhm  33938  xrge0pluscn  33939  cnzh  33969  rezh  33970  qqhval2lem  33982  esum0  34050  esumcst  34064  esumpcvgval  34079  esumcvg  34087  dmvlsiga  34130  measdivcstALTV  34226  eulerpartlemt  34373  coinfliprv  34485  ballotlem2  34491  signswmnd  34572  logdivsqrle  34665  hgt750lem  34666  bnj906  34944  indispconn  35239  cnllysconn  35250  rellysconn  35256  msrf  35547  brbigcup  35899  fobigcup  35901  brsingle  35918  fnsingle  35920  brimage  35927  funimage  35929  fnimage  35930  imageval  35931  brcart  35933  brapply  35939  brcup  35940  brcap  35941  funpartfun  35944  brub  35955  mpomulnzcnf  36300  onsucconni  36438  onsucsuccmpi  36444  dnicn  36493  bj-wnfnf  36740  bj-nnfv  36755  bj-nnfa1  36760  bj-nnfe1  36761  bj-rabtr  36931  taupilem2  37323  taupi  37324  f1omptsnlem  37337  icoreresf  37353  relowlpssretop  37365  finxpreclem3  37394  matunitlindf  37625  mblfinlem2  37665  areacirc  37720  0totbnd  37780  heiborlem6  37823  refrelid  38523  idsymrel  38562  trrelressn  38584  refrelsredund4  38633  refrelredund4  38636  disjALTV0  38755  disjALTVid  38756  antisymrelressn  38765  isolatiN  39217  isomliN  39240  ishlatiN  39356  mzpclall  42738  jm2.20nn  43009  dfacbasgrp  43120  dgraaf  43159  onexoegt  43256  omnord1  43318  oege2  43320  oenord1  43329  cantnftermord  43333  cantnf2  43338  omabs2  43345  omcl2  43346  ifpim3  43509  ifpim4  43511  ifpbi1b  43516  eu0  43533  omiscard  43556  iso0  44326  dvsid  44350  rankrelp  44977  halffl  45308  resincncf  45890  0cnf  45892  iblempty  45980  dirkeritg  46117  fourierdlem62  46183  fourierdlem76  46197  fourierdlem103  46224  etransclem18  46267  etransclem46  46295  abnotbtaxb  46927  dfaiota3  47104  sprsymrelf1  47483  fmtnof1  47522  fmtno4prm  47562  prmdvdsfmtnof1  47574  31prm  47584  requad01  47608  0evenALTV  47675  1oddALTV  47677  2evenALTV  47679  6even  47698  8even  47700  6gbe  47758  7gbow  47759  8gbe  47760  9gbo  47761  11gbo  47762  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2trifr  47996  gpg5grlic  48047  uspgrsprf1  48063  1odd  48087  nnsgrp  48093  0even  48153  2even  48155  2zrngamgm  48161  2zrngasgrp  48162  2zrngamnd  48163  2zrngagrp  48165  2zrngmsgrp  48169  zlmodzxzldeplem3  48419  lvecpsslmod  48424  ldepsnlinc  48425  blennngt2o2  48513  blennn0e2  48515  ackval42  48617  rrx2xpref1o  48639  rrx2plordisom  48644  sepfsepc  48825  setcsnterm  49133  setrec2lem2  49213  aacllem  49320