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  1338  euequ  2594  eqssi  4011  elini  4208  dtruALT2  5375  exexneq  5444  dtruOLD  5451  opnzi  5484  so0  5633  we0  5683  difxp  6185  ord0  6438  dfiota4  6554  funi  6599  funcnvsn  6617  idfn  6696  fn0  6699  f0  6789  fconst  6794  f10  6881  f1o0  6885  f1oi  6886  f1osn  6888  isoid  7348  porpss  7745  epweon  7793  epweonALT  7794  ordon  7795  omssnlim  7901  peano1  7910  fo1st  8032  fo2nd  8033  soseq  8182  wfrfunOLD  8357  wfr1OLD  8365  iordsmo  8395  tfrlem7  8421  tfr1  8435  frfnom  8473  seqomlem2  8489  oawordeulem  8590  1onn  8676  2onn  8678  naddf  8717  mapsnf1o2  8932  canth2  9168  1sdom2  9273  unfilem2  9341  cantnfvalf  9702  cnfcom3clem  9742  ssttrcl  9752  tc2  9779  r111  9812  rankf  9831  cardf2  9980  harcard  10015  r0weon  10049  infxpenc  10055  infxpenc2lem1  10056  alephon  10106  alephf1  10122  alephiso  10135  alephsmo  10139  alephf1ALT  10140  alephfplem4  10144  ackbij1lem17  10272  ackbij1  10274  ackbij2  10279  fin1a2lem2  10438  fin1a2lem4  10440  axcc2lem  10473  iunfo  10576  smobeth  10623  0tsk  10792  1pi  10920  nqerf  10967  axaddf  11182  axmulf  11183  axicn  11187  mpoaddf  11246  mpomulf  11247  mulnzcnf  11906  negiso  12245  dfnn2  12276  nnind  12281  0z  12621  dfuzi  12706  cnref1o  13024  elrpii  13034  0e0icopnf  13494  0e0iccpnf  13495  fldiv4p1lem1div2  13871  om2uzf1oi  13990  om2uzisoi  13991  uzrdgfni  13995  expcl2lem  14110  expclzlem  14120  expge0  14135  expge1  14136  faclbnd4lem1  14328  hashkf  14367  wwlktovf1  14992  sqrtf  15398  fclim  15585  fprodn0f  16023  eff2  16131  reeff1  16152  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  sin01gt0  16222  egt2lt3  16238  qnnen  16245  ruc  16275  halfleoddlt  16395  divalglem2  16428  divalglem9  16434  bitsf1  16479  sadaddlem  16499  2prm  16725  3prm  16727  1arith  16960  prmlem1a  17140  setsnid  17242  setsnidOLD  17243  xpsff1o  17613  dmaf  18102  cdaf  18103  coapm  18124  0pos  18378  0posOLD  18379  isposi  18381  letsr  18650  sgrp0b  18753  frmdplusg  18879  efmndsgrp  18911  smndex1sgrp  18933  smndex1mnd  18935  symg2bas  19424  pmtrsn  19551  odf  19569  efgsfo  19771  efgrelexlemb  19782  isabli  19828  rngmgpf  20174  mgpf  20265  prdscrngd  20335  xrsmgmdifsgrp  21438  xrs1cmn  21441  cnmgpid  21464  zringnzr  21488  zringunit  21494  zringlpir  21495  zringndrg  21496  pzriprnglem5  21513  pzriprnglem7  21515  pzriprnglem9  21517  pzriprnglem13  21521  zzngim  21588  cnmsgngrp  21614  psgninv  21617  zrhpsgnmhm  21619  retos  21653  refld  21654  rzgrp  21658  pjpm  21745  fntopon  22945  istpsi  22963  cmpfi  23431  indisconn  23441  kqf  23770  fbssfi  23860  zfbas  23919  ptcmplem2  24076  prdstmdd  24147  tsmsfbas  24151  ismeti  24350  prdsxmslem2  24557  cnfldms  24811  cnnrg  24816  tgqioo  24835  xrtgioo  24841  recld2  24849  xrge0gsumle  24868  xrge0tsms  24869  addcnlem  24899  divcnOLD  24903  divcn  24905  abscncf  24940  recncf  24941  imcncf  24942  cjcncf  24943  icopnfhmeo  24987  xrhmeo  24990  cnllycmp  25001  isclmi0  25144  iscvsi  25175  cnstrcvs  25187  cncms  25402  ovolf  25530  ovolre  25573  opnmblALT  25651  dveflem  26031  mdegxrf  26121  iaa  26381  ulmdm  26450  dvradcnv  26478  reeff1o  26505  reefiso  26506  reefgim  26508  recosf1o  26591  efifo  26603  logcn  26703  cxpcn3  26805  resqrtcn  26806  logb1  26826  logbmpt  26845  2logb9irrALT  26855  sqrt2cxp2logb9e3  26856  ressatans  26991  lgamcvg2  27112  lgam1  27121  gam1  27122  efnnfsumcl  27160  efchtdvds  27216  ppiub  27262  lgslem2  27356  lgsfcl2  27361  lgsne0  27393  2lgslem1b  27450  padicabvf  27689  bdayfo  27736  scutf  27871  madef  27909  scutfo  27956  addsf  28029  addsfo  28030  negsf  28098  negsfo  28099  negsf1o  28100  subsfo  28109  0ons  28293  1ons  28294  dfn0s2  28350  1nns  28366  nohalf  28421  0reno  28443  istrkg3ld  28483  axlowdimlem16  28986  upgrbi  29124  umgrbi  29132  lfuhgr1v0e  29285  cusgr0  29457  wlk2v2elem2  30184  upgr4cycl4dv4e  30213  konigsberglem4  30283  frgr0  30293  ex-pss  30456  ex-fl  30475  ex-mod  30477  isgrpoi  30526  grporn  30549  isabloi  30579  smcnlem  30725  lnocoi  30785  cncph  30847  cnbn  30897  cnchl  30944  norm3adifii  31176  hhph  31206  hhhl  31232  hlim0  31263  hlimf  31265  helch  31271  hsn0elch  31276  hhssabloilem  31289  hhssnv  31292  hhshsslem2  31296  hhssbnOLD  31307  shscli  31345  shintcli  31357  chintcli  31359  shsval2i  31415  pjhthlem2  31420  lejdii  31566  nonbooli  31679  pjrni  31730  pjfoi  31731  pjfi  31732  pjmf1  31744  df0op2  31780  idunop  32006  0cnop  32007  0cnfn  32008  idcnop  32009  idhmop  32010  0hmop  32011  0lnfn  32013  0bdop  32021  lnophsi  32029  lnopcoi  32031  lnopunii  32040  lnophmi  32046  nmcopex  32057  nmcoplb  32058  nmcfnex  32081  nmcfnlb  32082  imaelshi  32086  nlelshi  32088  nlelchi  32089  riesz4i  32091  riesz4  32092  riesz1  32093  cnlnadjlem6  32100  cnlnadjlem9  32103  cnlnadjeui  32105  cnlnadjeu  32106  nmopadji  32118  bdophsi  32124  bdopcoi  32126  nmopcoadji  32129  pjhmopi  32174  pjbdlni  32177  hmopidmchi  32179  mdslj1i  32347  rinvf1o  32646  nnindf  32825  rpdp2cl  32848  dp2ltc  32853  dpmul4  32880  s3clhash  32916  xrstos  32994  xrsclat  32995  xrge0tsmsd  33047  xrge0omnd  33070  cnfldfld  33350  reofld  33351  nn0archi  33354  zringidom  33558  zringfrac  33561  ccfldextrr  33675  ccfldsrarelvec  33695  ccfldextdgrr  33696  2sqr3minply  33752  xrge0iifmhm  33899  xrge0pluscn  33900  cnzh  33930  rezh  33931  qqhval2lem  33943  esum0  34029  esumcst  34043  esumpcvgval  34058  esumcvg  34066  dmvlsiga  34109  measdivcstALTV  34205  eulerpartlemt  34352  coinfliprv  34463  ballotlem2  34469  signswmnd  34550  logdivsqrle  34643  hgt750lem  34644  bnj906  34922  indispconn  35218  cnllysconn  35229  rellysconn  35235  msrf  35526  brbigcup  35879  fobigcup  35881  brsingle  35898  fnsingle  35900  brimage  35907  funimage  35909  fnimage  35910  imageval  35911  brcart  35913  brapply  35919  brcup  35920  brcap  35921  funpartfun  35924  brub  35935  mpomulnzcnf  36281  onsucconni  36419  onsucsuccmpi  36425  dnicn  36474  bj-wnfnf  36721  bj-nnfv  36736  bj-nnfa1  36741  bj-nnfe1  36742  bj-rabtr  36912  taupilem2  37304  taupi  37305  f1omptsnlem  37318  icoreresf  37334  relowlpssretop  37346  finxpreclem3  37375  matunitlindf  37604  mblfinlem2  37644  areacirc  37699  0totbnd  37759  heiborlem6  37802  refrelid  38503  idsymrel  38542  trrelressn  38564  refrelsredund4  38613  refrelredund4  38616  disjALTV0  38735  disjALTVid  38736  antisymrelressn  38745  isolatiN  39197  isomliN  39220  ishlatiN  39336  mzpclall  42714  jm2.20nn  42985  dfacbasgrp  43096  dgraaf  43135  onexoegt  43232  omnord1  43294  oege2  43296  oenord1  43305  cantnftermord  43309  cantnf2  43314  omabs2  43321  omcl2  43322  ifpim3  43485  ifpim4  43487  ifpbi1b  43492  eu0  43509  omiscard  43532  iso0  44302  dvsid  44326  halffl  45246  resincncf  45830  0cnf  45832  iblempty  45920  dirkeritg  46057  fourierdlem62  46123  fourierdlem76  46137  fourierdlem103  46164  etransclem18  46207  etransclem46  46235  abnotbtaxb  46864  dfaiota3  47041  sprsymrelf1  47420  fmtnof1  47459  fmtno4prm  47499  prmdvdsfmtnof1  47511  31prm  47521  requad01  47545  0evenALTV  47612  1oddALTV  47614  2evenALTV  47616  6even  47635  8even  47637  6gbe  47695  7gbow  47696  8gbe  47697  9gbo  47698  11gbo  47699  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2trifr  47931  gpg5grlic  47974  uspgrsprf1  47990  1odd  48014  nnsgrp  48020  0even  48080  2even  48082  2zrngamgm  48088  2zrngasgrp  48089  2zrngamnd  48090  2zrngagrp  48092  2zrngmsgrp  48096  zlmodzxzldeplem3  48347  lvecpsslmod  48352  ldepsnlinc  48353  blennngt2o2  48441  blennn0e2  48443  ackval42  48545  rrx2xpref1o  48567  rrx2plordisom  48572  sepfsepc  48723  setrec2lem2  48924  aacllem  49031