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  2594  eqssi  3947  elini  4148  dtruALT2  5310  exexneq  5379  opnzi  5417  so0  5565  we0  5614  difxp  6116  ord0  6365  dfiota4  6478  funi  6518  funcnvsn  6536  idfn  6614  fn0  6617  f0  6709  fconst  6714  f10  6801  f1o0  6805  f1oiOLD  6807  f1osn  6809  isoid  7269  porpss  7666  epweon  7714  epweonALT  7715  ordon  7716  omssnlim  7817  peano1  7825  fo1st  7947  fo2nd  7948  soseq  8095  iordsmo  8283  tfrlem7  8308  tfr1  8322  frfnom  8360  seqomlem2  8376  oawordeulem  8475  1onn  8561  2onn  8563  naddf  8602  mapsnf1o2  8824  canth2  9050  1sdom2  9139  unfilem2  9197  cantnfvalf  9562  cnfcom3clem  9602  ssttrcl  9612  tc2  9637  r111  9675  rankf  9694  cardf2  9843  harcard  9878  r0weon  9910  infxpenc  9916  infxpenc2lem1  9917  alephon  9967  alephf1  9983  alephiso  9996  alephsmo  10000  alephf1ALT  10001  alephfplem4  10005  ackbij1lem17  10133  ackbij1  10135  ackbij2  10140  fin1a2lem2  10299  fin1a2lem4  10301  axcc2lem  10334  iunfo  10437  smobeth  10484  0tsk  10653  1pi  10781  nqerf  10828  axaddf  11043  axmulf  11044  axicn  11048  mpoaddf  11107  mpomulf  11108  mulnzcnf  11770  negiso  12109  dfnn2  12145  nnind  12150  0z  12486  dfuzi  12570  cnref1o  12885  elrpii  12895  0e0icopnf  13360  0e0iccpnf  13361  fldiv4p1lem1div2  13741  om2uzf1oi  13862  om2uzisoi  13863  uzrdgfni  13867  expcl2lem  13982  expclzlem  13992  expge0  14007  expge1  14008  faclbnd4lem1  14202  hashkf  14241  wwlktovf1  14866  sqrtf  15273  fclim  15462  fprodn0f  15900  eff2  16010  reeff1  16031  ef01bndlem  16095  sin01bnd  16096  cos01bnd  16097  sin01gt0  16101  egt2lt3  16117  qnnen  16124  ruc  16154  halfleoddlt  16275  divalglem2  16308  divalglem9  16314  bitsf1  16359  sadaddlem  16379  2prm  16605  3prm  16607  1arith  16841  prmlem1a  17020  setsnid  17121  xpsff1o  17473  dmaf  17958  cdaf  17959  coapm  17980  0pos  18229  isposi  18231  letsr  18501  ex-chn1  18545  ex-chn2  18546  sgrp0b  18638  frmdplusg  18764  efmndsgrp  18796  smndex1sgrp  18818  smndex1mnd  18820  symg2bas  19307  pmtrsn  19433  odf  19451  efgsfo  19653  efgrelexlemb  19664  isabli  19710  rngmgpf  20077  mgpf  20168  prdscrngd  20242  xrsmgmdifsgrp  21347  cnmgpid  21368  xrs1cmn  21381  xrge0omnd  21384  zringnzr  21399  zringunit  21405  zringlpir  21406  zringndrg  21407  pzriprnglem5  21424  pzriprnglem7  21426  pzriprnglem9  21428  pzriprnglem13  21432  zzngim  21491  cnmsgngrp  21518  psgninv  21521  zrhpsgnmhm  21523  retos  21557  refld  21558  rzgrp  21562  pjpm  21647  fntopon  22840  istpsi  22858  cmpfi  23324  indisconn  23334  kqf  23663  fbssfi  23753  zfbas  23812  ptcmplem2  23969  prdstmdd  24040  tsmsfbas  24044  ismeti  24241  prdsxmslem2  24445  cnfldms  24691  cnnrg  24696  tgqioo  24716  xrtgioo  24723  recld2  24731  xrge0gsumle  24750  xrge0tsms  24751  addcnlem  24781  divcnOLD  24785  divcn  24787  abscncf  24822  recncf  24823  imcncf  24824  cjcncf  24825  icopnfhmeo  24869  xrhmeo  24872  cnllycmp  24883  isclmi0  25026  iscvsi  25057  cnstrcvs  25069  cncms  25283  ovolf  25411  ovolre  25454  opnmblALT  25532  dveflem  25911  mdegxrf  26001  iaa  26261  ulmdm  26330  dvradcnv  26358  reeff1o  26385  reefiso  26386  reefgim  26388  recosf1o  26472  efifo  26484  logcn  26584  cxpcn3  26686  resqrtcn  26687  logb1  26707  logbmpt  26726  2logb9irrALT  26736  sqrt2cxp2logb9e3  26737  ressatans  26872  lgamcvg2  26993  lgam1  27002  gam1  27003  efnnfsumcl  27041  efchtdvds  27097  ppiub  27143  lgslem2  27237  lgsfcl2  27242  lgsne0  27274  2lgslem1b  27331  padicabvf  27570  bdayfo  27617  scutf  27754  madef  27798  scutfo  27851  addsf  27926  addsfo  27927  negsf  27995  negsfo  27996  negsf1o  27997  subsfo  28006  0ons  28194  1ons  28195  onsiso  28206  dfn0s2  28261  1nns  28278  bdayn0sf1o  28296  zsoring  28333  twocut  28347  0reno  28400  istrkg3ld  28440  axlowdimlem16  28937  upgrbi  29073  umgrbi  29081  lfuhgr1v0e  29234  cusgr0  29406  wlk2v2elem2  30138  upgr4cycl4dv4e  30167  konigsberglem4  30237  frgr0  30247  ex-pss  30410  ex-fl  30429  ex-mod  30431  isgrpoi  30480  grporn  30503  isabloi  30533  smcnlem  30679  lnocoi  30739  cncph  30801  cnbn  30851  cnchl  30898  norm3adifii  31130  hhph  31160  hhhl  31186  hlim0  31217  hlimf  31219  helch  31225  hsn0elch  31230  hhssabloilem  31243  hhssnv  31246  hhshsslem2  31250  hhssbnOLD  31261  shscli  31299  shintcli  31311  chintcli  31313  shsval2i  31369  pjhthlem2  31374  lejdii  31520  nonbooli  31633  pjrni  31684  pjfoi  31685  pjfi  31686  pjmf1  31698  df0op2  31734  idunop  31960  0cnop  31961  0cnfn  31962  idcnop  31963  idhmop  31964  0hmop  31965  0lnfn  31967  0bdop  31975  lnophsi  31983  lnopcoi  31985  lnopunii  31994  lnophmi  32000  nmcopex  32011  nmcoplb  32012  nmcfnex  32035  nmcfnlb  32036  imaelshi  32040  nlelshi  32042  nlelchi  32043  riesz4i  32045  riesz4  32046  riesz1  32047  cnlnadjlem6  32054  cnlnadjlem9  32057  cnlnadjeui  32059  cnlnadjeu  32060  nmopadji  32072  bdophsi  32078  bdopcoi  32080  nmopcoadji  32083  pjhmopi  32128  pjbdlni  32131  hmopidmchi  32133  mdslj1i  32301  rinvf1o  32614  nnindf  32807  rpdp2cl  32869  dp2ltc  32874  dpmul4  32901  s3clhash  32936  xrstos  32998  xrsclat  32999  xrge0tsmsd  33049  qfld  33270  cnfldfld  33314  reofld  33315  nn0archi  33319  zringidom  33523  zringfrac  33526  ccfldextrr  33680  ccfldsrarelvec  33705  ccfldextdgrr  33706  2sqr3minply  33814  xrge0iifmhm  33973  xrge0pluscn  33974  cnzh  34002  rezh  34003  qqhval2lem  34015  esum0  34083  esumcst  34097  esumpcvgval  34112  esumcvg  34120  dmvlsiga  34163  measdivcstALTV  34259  eulerpartlemt  34405  coinfliprv  34517  ballotlem2  34523  signswmnd  34591  logdivsqrle  34684  hgt750lem  34685  bnj906  34963  fineqvnttrclse  35165  indispconn  35299  cnllysconn  35310  rellysconn  35316  msrf  35607  brbigcup  35961  fobigcup  35963  brsingle  35980  fnsingle  35982  brimage  35989  funimage  35991  fnimage  35992  imageval  35993  brcart  35995  brapply  36001  brcup  36002  brcap  36003  funpartfun  36008  brub  36019  mpomulnzcnf  36364  onsucconni  36502  onsucsuccmpi  36508  dnicn  36557  bj-wnfnf  36804  bj-nnfv  36819  bj-nnfa1  36824  bj-nnfe1  36825  bj-rabtr  36995  taupilem2  37387  taupi  37388  f1omptsnlem  37401  icoreresf  37417  relowlpssretop  37429  finxpreclem3  37458  matunitlindf  37678  mblfinlem2  37718  areacirc  37773  0totbnd  37833  heiborlem6  37876  dfsucmap3  38496  refrelid  38634  idsymrel  38677  trrelressn  38699  refrelsredund4  38748  refrelredund4  38751  disjALTV0  38872  disjALTVid  38873  antisymrelressn  38882  isolatiN  39335  isomliN  39358  ishlatiN  39474  mzpclall  42844  jm2.20nn  43114  dfacbasgrp  43225  dgraaf  43264  onexoegt  43361  omnord1  43422  oege2  43424  oenord1  43433  cantnftermord  43437  cantnf2  43442  omabs2  43449  omcl2  43450  ifpim3  43613  ifpim4  43615  ifpbi1b  43620  eu0  43637  omiscard  43660  iso0  44424  dvsid  44448  rankrelp  45077  halffl  45421  resincncf  45997  0cnf  45999  iblempty  46087  dirkeritg  46224  fourierdlem62  46290  fourierdlem76  46304  fourierdlem103  46331  etransclem18  46374  etransclem46  46402  abnotbtaxb  47039  dfaiota3  47216  ceilhalf1  47458  sprsymrelf1  47620  fmtnof1  47659  fmtno4prm  47699  prmdvdsfmtnof1  47711  31prm  47721  requad01  47745  0evenALTV  47812  1oddALTV  47814  2evenALTV  47816  6even  47835  8even  47837  6gbe  47895  7gbow  47896  8gbe  47897  9gbo  47898  11gbo  47899  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2trifr  48161  gpg5grlim  48217  gpg5grlic  48218  uspgrsprf1  48271  1odd  48295  nnsgrp  48301  0even  48361  2even  48363  2zrngamgm  48369  2zrngasgrp  48370  2zrngamnd  48371  2zrngagrp  48373  2zrngmsgrp  48377  zlmodzxzldeplem3  48627  lvecpsslmod  48632  ldepsnlinc  48633  blennngt2o2  48717  blennn0e2  48719  ackval42  48821  rrx2xpref1o  48843  rrx2plordisom  48848  slotresfo  49023  sepfsepc  49052  basresposfo  49102  oppff1  49273  setcsnterm  49615  setc1onsubc  49727  setrec2lem2  49819  aacllem  49926