Theorem mpbir2an 723

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3pm3.2i  1356  euequ  2627  eqssi  3955  elini  4154  dtruALT2  5332  exexneq  5407  opnzi  5447  so0  5598  we0  5647  difxp  6153  ord0  6404  dfiota4  6517  funi  6557  funcnvsn  6575  idfn  6653  fn0  6656  f0  6749  fconst  6754  f10  6844  f1o0  6848  f1oiOLD  6850  f1osn  6852  isoid  7317  porpss  7714  epweon  7762  epweonALT  7763  ordon  7764  omssnlim  7865  peano1  7873  fo1st  7994  fo2nd  7995  soseq  8143  iordsmo  8332  tfrlem7  8358  tfr1  8372  frfnom  8410  seqomlem2  8426  oawordeulem  8527  1onn  8614  2onn  8616  naddf  8656  mapsnf1o2  8880  canth2  9106  1sdom2  9196  unfilem2  9254  cantnfvalf  9622  cnfcom3clem  9662  ssttrcl  9672  tc2  9697  r111  9735  rankf  9754  cardf2  9917  harcard  9952  r0weon  9984  infxpenc  9990  infxpenc2lem1  9991  alephon  10041  alephf1  10057  alephiso  10070  alephsmo  10074  alephf1ALT  10075  alephfplem4  10079  ackbij1lem17  10206  ackbij1  10208  ackbij2  10213  fin1a2lem2  10373  fin1a2lem4  10375  axcc2lem  10408  iunfo  10511  smobeth  10559  0tsk  10728  1pi  10856  nqerf  10903  axaddf  11118  axmulf  11119  axicn  11123  mpoaddf  11182  mpomulf  11183  mulnzcnf  11848  negiso  12186  dfnn2  12237  nnind  12242  0z  12593  dfuzi  12678  cnref1o  13000  elrpii  13010  0e0icopnf  13476  0e0iccpnf  13477  fldiv4p1lem1div2  13859  om2uzf1oi  13980  om2uzisoi  13981  uzrdgfni  13985  expcl2lem  14100  expclzlem  14110  expge0  14125  expge1  14126  faclbnd4lem1  14320  hashkf  14359  wwlktovf1  14984  sgnfo  15126  sqrtf  15405  fclim  15594  fprodn0f  16035  eff2  16145  reeff1  16166  ef01bndlem  16230  sin01bnd  16231  cos01bnd  16232  sin01gt0  16236  egt2lt3  16252  qnnen  16259  ruc  16289  halfleoddlt  16410  divalglem2  16443  divalglem9  16449  bitsf1  16494  sadaddlem  16514  2prm  16740  3prm  16742  1arith  16977  prmlem1a  17156  setsnid  17258  xpsff1o  17611  dmaf  18096  cdaf  18097  coapm  18118  0pos  18367  isposi  18369  letsr  18639  ex-chn1  18683  ex-chn2  18684  sgrp0b  18776  frmdplusg  18903  efmndsgrp  18935  smndex1sgrp  18960  smndex1mnd  18962  symg2bas  19454  pmtrsn  19580  odf  19598  efgsfo  19800  efgrelexlemb  19811  isabli  19857  rngmgpf  20226  mgpf  20321  prdscrngd  20394  xrsmgmdifsgrp  21519  cnmgpid  21539  xrs1cmn  21552  xrge0omnd  21555  zringnzr  21570  zringunit  21576  zringlpir  21577  zringndrg  21578  pzriprnglem5  21595  pzriprnglem7  21597  pzriprnglem9  21599  pzriprnglem13  21603  zzngim  21662  cnmsgngrp  21689  psgninv  21692  zrhpsgnmhm  21694  retos  21728  refld  21729  rzgrp  21733  pjpm  21818  fntopon  23042  istpsi  23060  cmpfi  23526  indisconn  23536  kqf  23865  fbssfi  23955  zfbas  24014  ptcmplem2  24171  prdstmdd  24242  tsmsfbas  24246  ismeti  24443  prdsxmslem2  24647  cnfldms  24893  cnnrg  24898  tgqioo  24918  xrtgioo  24925  recld2  24933  xrge0gsumle  24952  xrge0tsms  24953  addcnlem  24983  divcn  24988  abscncf  25021  recncf  25022  imcncf  25023  cjcncf  25024  icopnfhmeo  25063  xrhmeo  25066  cnllycmp  25076  isclmi0  25218  iscvsi  25249  cnstrcvs  25261  cncms  25475  ovolf  25602  ovolre  25645  opnmblALT  25723  dveflem  26099  mdegxrf  26186  iaa  26447  ulmdm  26514  dvradcnv  26542  reeff1o  26568  reefiso  26569  reefgim  26571  recosf1o  26658  efifo  26670  logcn  26770  cxpcn3  26871  resqrtcn  26872  logb1  26892  logbmpt  26911  2logb9irrALT  26921  sqrt2cxp2logb9e3  26922  ressatans  27057  lgamcvg2  27177  lgam1  27186  gam1  27187  efnnfsumcl  27225  efchtdvds  27281  ppiub  27326  lgslem2  27420  lgsfcl2  27425  lgsne0  27457  2lgslem1b  27514  padicabvf  27753  bdayfo  27799  cutsf  27943  madef  27987  cutsfo  28056  addsf  28133  addsfo  28134  negsf  28203  negsfo  28204  negsf1o  28205  subsfo  28216  0ons  28407  1ons  28408  oniso  28422  dfn0s2  28483  1nns  28500  bdayn0sf1o  28521  zsoring  28560  twocut  28574  0reno  28647  1reno  28648  istrkg3ld  28688  axlowdimlem16  29216  upgrbi  29352  umgrbi  29360  lfuhgr1v0e  29513  cusgr0  29685  wlk2v2elem2  30416  upgr4cycl4dv4e  30445  konigsberglem4  30515  frgr0  30525  ex-pss  30688  ex-fl  30707  ex-mod  30709  isgrpoi  30759  grporn  30782  isabloi  30812  smcnlem  30958  lnocoi  31018  cncph  31080  cnbn  31130  cnchl  31177  norm3adifii  31409  hhph  31439  hhhl  31465  hlim0  31496  hlimf  31498  helch  31504  hsn0elch  31509  hhssabloilem  31522  hhssnv  31525  hhshsslem2  31529  hhssbnOLD  31540  shscli  31578  shintcli  31590  chintcli  31592  shsval2i  31648  pjhthlem2  31653  lejdii  31799  nonbooli  31912  pjrni  31963  pjfoi  31964  pjfi  31965  pjmf1  31977  df0op2  32013  idunop  32239  0cnop  32240  0cnfn  32241  idcnop  32242  idhmop  32243  0hmop  32244  0lnfn  32246  0bdop  32254  lnophsi  32262  lnopcoi  32264  lnopunii  32273  lnophmi  32279  nmcopex  32290  nmcoplb  32291  nmcfnex  32314  nmcfnlb  32315  imaelshi  32319  nlelshi  32321  nlelchi  32322  riesz4i  32324  riesz4  32325  riesz1  32326  cnlnadjlem6  32333  cnlnadjlem9  32336  cnlnadjeui  32338  cnlnadjeu  32339  nmopadji  32351  bdophsi  32357  bdopcoi  32359  nmopcoadji  32362  pjhmopi  32407  pjbdlni  32410  hmopidmchi  32412  mdslj1i  32580  rinvf1o  32887  nnindf  33077  rpdp2cl  33114  dp2ltc  33119  dpmul4  33146  s3clhash  33181  xrstos  33243  xrsclat  33244  xrge0tsmsd  33306  qfld  33533  cnfldfld  33577  reofld  33578  nn0archi  33582  zringidom  33758  zringfrac  33761  ccfldextrr  33953  ccfldsrarelvec  33978  ccfldextdgrr  33979  2sqr3minply  34087  xrge0iifmhm  34246  xrge0pluscn  34247  cnzh  34275  rezh  34276  qqhval2lem  34288  esum0  34356  esumcst  34370  esumpcvgval  34385  esumcvg  34393  dmvlsiga  34436  measdivcstALTV  34532  eulerpartlemt  34678  coinfliprv  34790  ballotlem2  34796  signswmnd  34861  logdivsqrle  34954  hgt750lem  34955  bnj906  35235  xoromon  35394  fineqvnttrclse  35432  indispconn  35597  cnllysconn  35608  rellysconn  35614  msrf  35905  brbigcup  36259  fobigcup  36261  brsingle  36278  fnsingle  36280  brimage  36287  funimage  36289  fnimage  36290  imageval  36291  brcart  36293  brapply  36299  brcup  36300  brcap  36301  funpartfun  36306  brub  36317  mpomulnzcnf  36672  onsucconni  36810  onsucsuccmpi  36816  dnicn  36943  bj-nnfv  37255  bj-wnfnf  37270  bj-nnfa1  37271  bj-nnfe1  37272  bj-rabtr  37427  bj-axreprepsep  37572  taupilem2  37826  taupi  37827  f1omptsnlem  37842  icoreresf  37858  relowlpssretop  37870  finxpreclem3  37899  matunitlindf  38129  mblfinlem2  38169  areacirc  38224  0totbnd  38284  heiborlem6  38327  dfsucmap3  38974  refrelid  39113  idsymrel  39156  trrelressn  39178  refrelsredund4  39227  refrelredund4  39230  disjALTV0  39365  disjALTVid  39366  antisymrelressn  39378  isolatiN  39852  isomliN  39875  ishlatiN  39991  mzpclall  43320  jm2.20nn  43586  dfacbasgrp  43697  dgraaf  43736  onexoegt  43833  omnord1  43894  oege2  43896  oenord1  43905  cantnftermord  43909  cantnf2  43914  omabs2  43921  omcl2  43922  ifpim3  44084  ifpim4  44086  ifpbi1b  44091  eu0  44108  omiscard  44131  iso0  44881  dvsid  44905  rankrelp  45534  halffl  45873  resincncf  46447  0cnf  46449  iblempty  46537  dirkeritg  46674  fourierdlem62  46740  fourierdlem76  46754  fourierdlem103  46781  etransclem18  46824  etransclem46  46852  abnotbtaxb  47507  dfaiota3  47684  ceilhalf1  47930  sprsymrelf1  48100  fmtnof1  48142  fmtno4prm  48182  prmdvdsfmtnof1  48194  31prm  48204  requad01  48241  0evenALTV  48308  1oddALTV  48310  2evenALTV  48312  6even  48331  8even  48333  6gbe  48391  7gbow  48392  8gbe  48393  9gbo  48394  11gbo  48395  usgrexmpl1lem  48641  usgrexmpl2lem  48646  usgrexmpl2trifr  48657  gpg5grlim  48713  gpg5grlic  48714  uspgrsprf1  48767  1odd  48791  nnsgrp  48797  0even  48857  2even  48859  2zrngamgm  48865  2zrngasgrp  48866  2zrngamnd  48867  2zrngagrp  48869  2zrngmsgrp  48873  zlmodzxzldeplem3  49133  lvecpsslmod  49138  ldepsnlinc  49139  blennngt2o2  49223  blennn0e2  49225  ackval42  49327  rrx2xpref1o  49349  rrx2plordisom  49354  slotresfo  49528  sepfsepc  49557  basresposfo  49607  oppff1  49777  setcsnterm  50119  setc1onsubc  50231  setrec2lem2  50323  aacllem  50430