Theorem mpbir2an 708

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  3pm3.2i  1338  euequ  2595  eqssi  3948  elini  4140  dtruALT2  5313  exexneq  5379  dtruOLD  5386  opnzi  5419  so0  5568  we0  5615  difxp  6102  ord0  6354  dfiota4  6471  funi  6516  funcnvsn  6534  idfn  6612  fn0  6615  f0  6706  fconst  6711  f10  6800  f1o0  6804  f1oi  6805  f1osn  6807  isoid  7256  porpss  7642  epweon  7687  epweonALT  7688  ordon  7689  omssnlim  7795  peano1  7803  fo1st  7919  fo2nd  7920  soseq  8046  wfrfunOLD  8220  wfr1OLD  8228  iordsmo  8258  tfrlem7  8284  tfr1  8298  frfnom  8336  seqomlem2  8352  oawordeulem  8456  1onn  8541  2onn  8543  mapsnf1o2  8753  canth2  8995  1sdom2  9105  unfilem2  9176  cantnfvalf  9522  cnfcom3clem  9562  ssttrcl  9572  tc2  9599  r111  9632  rankf  9651  cardf2  9800  harcard  9835  r0weon  9869  infxpenc  9875  infxpenc2lem1  9876  alephon  9926  alephf1  9942  alephiso  9955  alephsmo  9959  alephf1ALT  9960  alephfplem4  9964  ackbij1lem17  10093  ackbij1  10095  ackbij2  10100  fin1a2lem2  10258  fin1a2lem4  10260  axcc2lem  10293  iunfo  10396  smobeth  10443  0tsk  10612  1pi  10740  nqerf  10787  axaddf  11002  axmulf  11003  axicn  11007  mulnzcnopr  11722  negiso  12056  dfnn2  12087  nnind  12092  0z  12431  dfuzi  12512  cnref1o  12826  elrpii  12834  0e0icopnf  13291  0e0iccpnf  13292  fz0to4untppr  13460  fldiv4p1lem1div2  13656  om2uzf1oi  13774  om2uzisoi  13775  uzrdgfni  13779  expcl2lem  13895  expclzlem  13907  expge0  13920  expge1  13921  faclbnd4lem1  14108  hashkf  14147  wwlktovf1  14771  sqrtf  15174  fclim  15361  fprodn0f  15800  eff2  15907  reeff1  15928  ef01bndlem  15992  sin01bnd  15993  cos01bnd  15994  sin01gt0  15998  egt2lt3  16014  qnnen  16021  ruc  16051  halfleoddlt  16170  divalglem2  16203  divalglem9  16209  bitsf1  16252  sadaddlem  16272  2prm  16494  3prm  16496  1arith  16725  prmlem1a  16905  setsnid  17007  setsnidOLD  17008  xpsff1o  17375  dmaf  17861  cdaf  17862  coapm  17883  0pos  18136  0posOLD  18137  isposi  18139  letsr  18408  sgrp0b  18480  frmdplusg  18589  efmndsgrp  18621  smndex1sgrp  18643  smndex1mnd  18645  symg2bas  19096  pmtrsn  19223  odf  19241  efgsfo  19440  efgrelexlemb  19451  isabli  19496  mgpf  19893  prdscrngd  19947  xrsmgmdifsgrp  20741  xrs1cmn  20744  cnmgpid  20766  zringnzr  20788  zringunit  20794  zringlpir  20795  zringndrg  20796  zzngim  20866  cnmsgngrp  20890  psgninv  20893  zrhpsgnmhm  20895  retos  20929  refld  20930  rzgrp  20934  pjpm  21021  fntopon  22179  istpsi  22197  cmpfi  22665  indisconn  22675  kqf  23004  fbssfi  23094  zfbas  23153  ptcmplem2  23310  prdstmdd  23381  tsmsfbas  23385  ismeti  23584  prdsxmslem2  23791  cnfldms  24045  cnnrg  24050  tgqioo  24069  xrtgioo  24075  recld2  24083  xrge0gsumle  24102  xrge0tsms  24103  addcnlem  24133  divcn  24137  abscncf  24170  recncf  24171  imcncf  24172  cjcncf  24173  icopnfhmeo  24212  xrhmeo  24215  cnllycmp  24225  isclmi0  24367  iscvsi  24398  cnstrcvs  24410  cncms  24625  ovolf  24752  ovolre  24795  opnmblALT  24873  dveflem  25249  mdegxrf  25339  iaa  25591  ulmdm  25658  dvradcnv  25686  reeff1o  25712  reefiso  25713  reefgim  25715  recosf1o  25797  efifo  25809  logcn  25908  cxpcn3  26007  resqrtcn  26008  logb1  26025  logbmpt  26044  2logb9irrALT  26054  sqrt2cxp2logb9e3  26055  ressatans  26190  lgamcvg2  26310  lgam1  26319  gam1  26320  efnnfsumcl  26358  efchtdvds  26414  ppiub  26458  lgslem2  26552  lgsfcl2  26557  lgsne0  26589  2lgslem1b  26646  padicabvf  26885  bdayfo  26931  scutf  27057  istrkg3ld  27111  axlowdimlem16  27614  upgrbi  27752  umgrbi  27760  lfuhgr1v0e  27910  cusgr0  28082  wlk2v2elem2  28808  upgr4cycl4dv4e  28837  konigsberglem4  28907  frgr0  28917  ex-pss  29080  ex-fl  29099  ex-mod  29101  isgrpoi  29148  grporn  29171  isabloi  29201  smcnlem  29347  lnocoi  29407  cncph  29469  cnbn  29519  cnchl  29566  norm3adifii  29798  hhph  29828  hhhl  29854  hlim0  29885  hlimf  29887  helch  29893  hsn0elch  29898  hhssabloilem  29911  hhssnv  29914  hhshsslem2  29918  hhssbnOLD  29929  shscli  29967  shintcli  29979  chintcli  29981  shsval2i  30037  pjhthlem2  30042  lejdii  30188  nonbooli  30301  pjrni  30352  pjfoi  30353  pjfi  30354  pjmf1  30366  df0op2  30402  idunop  30628  0cnop  30629  0cnfn  30630  idcnop  30631  idhmop  30632  0hmop  30633  0lnfn  30635  0bdop  30643  lnophsi  30651  lnopcoi  30653  lnopunii  30662  lnophmi  30668  nmcopex  30679  nmcoplb  30680  nmcfnex  30703  nmcfnlb  30704  imaelshi  30708  nlelshi  30710  nlelchi  30711  riesz4i  30713  riesz4  30714  riesz1  30715  cnlnadjlem6  30722  cnlnadjlem9  30725  cnlnadjeui  30727  cnlnadjeu  30728  nmopadji  30740  bdophsi  30746  bdopcoi  30748  nmopcoadji  30751  pjhmopi  30796  pjbdlni  30799  hmopidmchi  30801  mdslj1i  30969  rinvf1o  31252  nnindf  31420  rpdp2cl  31443  dp2ltc  31448  dpmul4  31475  s3clhash  31509  xrstos  31575  xrsclat  31576  xrge0tsmsd  31604  xrge0omnd  31624  reofld  31840  nn0archi  31843  ccfldextrr  32021  ccfldsrarelvec  32039  ccfldextdgrr  32040  xrge0iifmhm  32187  xrge0pluscn  32188  cnzh  32218  rezh  32219  qqhval2lem  32229  esum0  32315  esumcst  32329  esumpcvgval  32344  esumcvg  32352  dmvlsiga  32395  measdivcstALTV  32491  eulerpartlemt  32638  coinfliprv  32749  ballotlem2  32755  signswmnd  32836  logdivsqrle  32930  hgt750lem  32931  bnj906  33209  indispconn  33495  cnllysconn  33506  rellysconn  33512  msrf  33803  madef  34136  scutfo  34180  brbigcup  34296  fobigcup  34298  brsingle  34315  fnsingle  34317  brimage  34324  funimage  34326  fnimage  34327  imageval  34328  brcart  34330  brapply  34336  brcup  34337  brcap  34338  funpartfun  34341  brub  34352  onsucconni  34722  onsucsuccmpi  34728  dnicn  34768  bj-wnfnf  35017  bj-nnfv  35032  bj-nnfa1  35037  bj-nnfe1  35038  bj-rabtr  35213  taupilem2  35598  taupi  35599  f1omptsnlem  35612  icoreresf  35628  relowlpssretop  35640  finxpreclem3  35669  matunitlindf  35880  mblfinlem2  35920  areacirc  35975  0totbnd  36036  heiborlem6  36079  refrelid  36789  idsymrel  36828  trrelressn  36850  refrelsredund4  36899  refrelredund4  36902  disjALTV0  37021  disjALTVid  37022  antisymrelressn  37031  isolatiN  37483  isomliN  37506  ishlatiN  37622  mzpclall  40811  jm2.20nn  41082  dfacbasgrp  41196  dgraaf  41235  omabs2  41317  omcl2  41318  ifpim3  41425  ifpim4  41427  ifpbi1b  41432  eu0  41449  omiscard  41472  iso0  42246  dvsid  42270  halffl  43170  resincncf  43752  0cnf  43754  iblempty  43842  dirkeritg  43979  fourierdlem62  44045  fourierdlem76  44059  fourierdlem103  44086  etransclem18  44129  etransclem46  44157  abnotbtaxb  44761  dfaiota3  44935  sprsymrelf1  45299  fmtnof1  45338  fmtno4prm  45378  prmdvdsfmtnof1  45390  31prm  45400  requad01  45424  0evenALTV  45491  1oddALTV  45493  2evenALTV  45495  6even  45514  8even  45516  6gbe  45574  7gbow  45575  8gbe  45576  9gbo  45577  11gbo  45578  uspgrsprf1  45660  1odd  45716  nnsgrp  45722  0even  45840  2even  45842  2zrngamgm  45848  2zrngasgrp  45849  2zrngamnd  45850  2zrngagrp  45852  2zrngmsgrp  45856  zlmodzxzldeplem3  46194  lvecpsslmod  46199  ldepsnlinc  46200  blennngt2o2  46289  blennn0e2  46291  ackval42  46393  rrx2xpref1o  46415  rrx2plordisom  46420  sepfsepc  46572  setrec2lem2  46751  aacllem  46856