Theorem mpbir2an 709

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  3pm3.2i  1335  equsb1vOLDOLD  2513  sbtvOLD  2515  euequ  2679  eqssi  3982  elini  4169  dtru  5263  opnzi  5358  so0  5503  we0  5544  difxp  6015  ord0  6237  dfiota4  6341  funi  6381  funcnvsn  6398  idfn  6469  fnresiOLD  6471  fn0  6473  f0  6554  fconst  6559  f10  6641  f1o0  6645  f1oi  6646  f1osn  6648  isoid  7076  porpss  7447  epweon  7491  ordon  7492  omssnlim  7588  fo1st  7703  fo2nd  7704  wfrfun  7959  wfr1  7967  iordsmo  7988  tfrlem7  8013  tfr1  8027  frfnom  8064  seqomlem2  8081  oawordeulem  8174  mapsnf1o2  8452  canth2  8664  unfilem2  8777  cantnfvalf  9122  cnfcom3clem  9162  tc2  9178  r111  9198  rankf  9217  cardf2  9366  harcard  9401  r0weon  9432  infxpenc  9438  infxpenc2lem1  9439  alephon  9489  alephf1  9505  alephiso  9518  alephsmo  9522  alephf1ALT  9523  alephfplem4  9527  ackbij1lem17  9652  ackbij1  9654  ackbij2  9659  fin1a2lem2  9817  fin1a2lem4  9819  axcc2lem  9852  iunfo  9955  smobeth  10002  0tsk  10171  1pi  10299  nqerf  10346  axaddf  10561  axmulf  10562  axicn  10566  mulnzcnopr  11280  negiso  11615  dfnn2  11645  nnind  11650  0z  11986  dfuzi  12067  cnref1o  12378  elrpii  12386  0e0icopnf  12840  0e0iccpnf  12841  fz0to4untppr  13004  fldiv4p1lem1div2  13199  om2uzf1oi  13315  om2uzisoi  13316  uzrdgfni  13320  expcl2lem  13435  expclzlem  13447  expge0  13459  expge1  13460  faclbnd4lem1  13647  hashkf  13686  wwlktovf1  14315  sqrtf  14717  fclim  14904  fprodn0f  15339  eff2  15446  reeff1  15467  ef01bndlem  15531  sin01bnd  15532  cos01bnd  15533  sin01gt0  15537  egt2lt3  15553  qnnen  15560  ruc  15590  halfleoddlt  15705  divalglem2  15740  divalglem9  15746  bitsf1  15789  sadaddlem  15809  2prm  16030  3prm  16032  1arith  16257  prmlem1a  16434  setsnid  16533  xpsff1o  16834  dmaf  17303  cdaf  17304  coapm  17325  0pos  17558  isposi  17560  letsr  17831  sgrp0b  17903  frmdplusg  18013  efmndsgrp  18045  smndex1sgrp  18067  smndex1mnd  18069  symg2bas  18515  pmtrsn  18641  odf  18659  efgsfo  18859  efgrelexlemb  18870  isabli  18915  mgpf  19303  prdscrngd  19357  xrsmgmdifsgrp  20576  xrs1cmn  20579  cnmgpid  20601  zringnzr  20623  zringunit  20629  zringlpir  20630  zringndrg  20631  zzngim  20693  cnmsgngrp  20717  psgninv  20720  zrhpsgnmhm  20722  retos  20756  refld  20757  rzgrp  20761  pjpm  20846  fntopon  21526  istpsi  21544  cmpfi  22010  indisconn  22020  kqf  22349  fbssfi  22439  zfbas  22498  ptcmplem2  22655  prdstmdd  22726  tsmsfbas  22730  ismeti  22929  prdsxmslem2  23133  cnfldms  23378  cnnrg  23383  tgqioo  23402  xrtgioo  23408  recld2  23416  xrge0gsumle  23435  xrge0tsms  23436  addcnlem  23466  divcn  23470  abscncf  23503  recncf  23504  imcncf  23505  cjcncf  23506  icopnfhmeo  23541  xrhmeo  23544  cnllycmp  23554  isclmi0  23696  iscvsi  23727  cnstrcvs  23739  cncms  23952  ovolf  24077  ovolre  24120  opnmblALT  24198  dveflem  24570  mdegxrf  24656  iaa  24908  ulmdm  24975  dvradcnv  25003  reeff1o  25029  reefiso  25030  reefgim  25032  recosf1o  25113  efifo  25125  logcn  25224  cxpcn3  25323  resqrtcn  25324  logb1  25341  logbmpt  25360  2logb9irrALT  25370  sqrt2cxp2logb9e3  25371  ressatans  25506  lgamcvg2  25626  lgam1  25635  gam1  25636  efnnfsumcl  25674  efchtdvds  25730  ppiub  25774  lgslem2  25868  lgsfcl2  25873  lgsne0  25905  2lgslem1b  25962  padicabvf  26201  istrkg3ld  26241  axlowdimlem16  26737  upgrbi  26872  umgrbi  26880  lfuhgr1v0e  27030  cusgr0  27202  wlk2v2elem2  27929  upgr4cycl4dv4e  27958  konigsberglem4  28028  frgr0  28038  ex-pss  28201  ex-fl  28220  ex-mod  28222  isgrpoi  28269  grporn  28292  isabloi  28322  smcnlem  28468  lnocoi  28528  cncph  28590  cnbn  28640  cnchl  28687  norm3adifii  28919  hhph  28949  hhhl  28975  hlim0  29006  hlimf  29008  helch  29014  hsn0elch  29019  hhssabloilem  29032  hhssnv  29035  hhshsslem2  29039  hhssbnOLD  29050  shscli  29088  shintcli  29100  chintcli  29102  shsval2i  29158  pjhthlem2  29163  lejdii  29309  nonbooli  29422  pjrni  29473  pjfoi  29474  pjfi  29475  pjmf1  29487  df0op2  29523  idunop  29749  0cnop  29750  0cnfn  29751  idcnop  29752  idhmop  29753  0hmop  29754  0lnfn  29756  0bdop  29764  lnophsi  29772  lnopcoi  29774  lnopunii  29783  lnophmi  29789  nmcopex  29800  nmcoplb  29801  nmcfnex  29824  nmcfnlb  29825  imaelshi  29829  nlelshi  29831  nlelchi  29832  riesz4i  29834  riesz4  29835  riesz1  29836  cnlnadjlem6  29843  cnlnadjlem9  29846  cnlnadjeui  29848  cnlnadjeu  29849  nmopadji  29861  bdophsi  29867  bdopcoi  29869  nmopcoadji  29872  pjhmopi  29917  pjbdlni  29920  hmopidmchi  29922  mdslj1i  30090  rinvf1o  30369  nnindf  30529  rpdp2cl  30553  dp2ltc  30558  dpmul4  30585  s3clhash  30619  xrstos  30661  xrsclat  30662  xrge0tsmsd  30687  xrge0omnd  30707  reofld  30908  nn0archi  30911  ccfldextrr  31033  ccfldsrarelvec  31051  ccfldextdgrr  31052  xrge0iifmhm  31177  xrge0pluscn  31178  cnzh  31206  rezh  31207  qqhval2lem  31217  esum0  31303  esumcst  31317  esumpcvgval  31332  esumcvg  31340  dmvlsiga  31383  measdivcstALTV  31479  eulerpartlemt  31624  coinfliprv  31735  ballotlem2  31741  signswmnd  31822  logdivsqrle  31916  hgt750lem  31917  bnj906  32197  indispconn  32476  cnllysconn  32487  rellysconn  32493  msrf  32784  soseq  33091  bdayfo  33177  scutf  33268  brbigcup  33354  fobigcup  33356  brsingle  33373  fnsingle  33375  brimage  33382  funimage  33384  fnimage  33385  imageval  33386  brcart  33388  brapply  33394  brcup  33395  brcap  33396  funpartfun  33399  brub  33410  onsucconni  33780  onsucsuccmpi  33786  dnicn  33826  bj-wnfnf  34063  bj-nnfv  34078  bj-nnfa1  34083  bj-nnfe1  34084  bj-dtru  34134  bj-rabtr  34243  taupilem2  34597  taupi  34598  f1omptsnlem  34611  icoreresf  34627  relowlpssretop  34639  finxpreclem3  34668  matunitlindf  34884  mblfinlem2  34924  areacirc  34981  0totbnd  35045  heiborlem6  35088  refrelid  35755  idsymrel  35791  refrelsredund4  35861  refrelredund4  35864  disjALTV0  35978  disjALTVid  35979  isolatiN  36346  isomliN  36369  ishlatiN  36485  sn-dtru  39104  mzpclall  39317  jm2.20nn  39587  dfacbasgrp  39701  dgraaf  39740  ifpim3  39855  ifpim4  39857  ifpbi1b  39862  eu0  39879  iso0  40632  dvsid  40656  halffl  41556  resincncf  42151  0cnf  42153  iblempty  42243  dirkeritg  42381  fourierdlem62  42447  fourierdlem76  42461  fourierdlem103  42488  etransclem18  42531  etransclem46  42559  abnotbtaxb  43145  sprsymrelf1  43652  fmtnof1  43691  fmtno4prm  43731  prmdvdsfmtnof1  43743  31prm  43754  requad01  43780  0evenALTV  43847  1oddALTV  43849  2evenALTV  43851  6even  43870  8even  43872  6gbe  43930  7gbow  43931  8gbe  43932  9gbo  43933  11gbo  43934  uspgrsprf1  44016  1odd  44072  nnsgrp  44078  0even  44196  2even  44198  2zrngamgm  44204  2zrngasgrp  44205  2zrngamnd  44206  2zrngagrp  44208  2zrngmsgrp  44212  zlmodzxzldeplem3  44551  lvecpsslmod  44556  ldepsnlinc  44557  blennngt2o2  44646  blennn0e2  44648  rrx2xpref1o  44699  rrx2plordisom  44704  setrec2lem2  44791  aacllem  44896