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  2590  eqssi  3963  elini  4162  dtruALT2  5325  exexneq  5394  dtruOLD  5401  opnzi  5434  so0  5584  we0  5633  difxp  6137  ord0  6386  dfiota4  6503  funi  6548  funcnvsn  6566  idfn  6646  fn0  6649  f0  6741  fconst  6746  f10  6833  f1o0  6837  f1oi  6838  f1osn  6840  isoid  7304  porpss  7703  epweon  7751  epweonALT  7752  ordon  7753  omssnlim  7857  peano1  7865  fo1st  7988  fo2nd  7989  soseq  8138  iordsmo  8326  tfrlem7  8351  tfr1  8365  frfnom  8403  seqomlem2  8419  oawordeulem  8518  1onn  8604  2onn  8606  naddf  8645  mapsnf1o2  8867  canth2  9094  1sdom2  9187  unfilem2  9255  cantnfvalf  9618  cnfcom3clem  9658  ssttrcl  9668  tc2  9695  r111  9728  rankf  9747  cardf2  9896  harcard  9931  r0weon  9965  infxpenc  9971  infxpenc2lem1  9972  alephon  10022  alephf1  10038  alephiso  10051  alephsmo  10055  alephf1ALT  10056  alephfplem4  10060  ackbij1lem17  10188  ackbij1  10190  ackbij2  10195  fin1a2lem2  10354  fin1a2lem4  10356  axcc2lem  10389  iunfo  10492  smobeth  10539  0tsk  10708  1pi  10836  nqerf  10883  axaddf  11098  axmulf  11099  axicn  11103  mpoaddf  11162  mpomulf  11163  mulnzcnf  11824  negiso  12163  dfnn2  12199  nnind  12204  0z  12540  dfuzi  12625  cnref1o  12944  elrpii  12954  0e0icopnf  13419  0e0iccpnf  13420  fldiv4p1lem1div2  13797  om2uzf1oi  13918  om2uzisoi  13919  uzrdgfni  13923  expcl2lem  14038  expclzlem  14048  expge0  14063  expge1  14064  faclbnd4lem1  14258  hashkf  14297  wwlktovf1  14923  sqrtf  15330  fclim  15519  fprodn0f  15957  eff2  16067  reeff1  16088  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  sin01gt0  16158  egt2lt3  16174  qnnen  16181  ruc  16211  halfleoddlt  16332  divalglem2  16365  divalglem9  16371  bitsf1  16416  sadaddlem  16436  2prm  16662  3prm  16664  1arith  16898  prmlem1a  17077  setsnid  17178  xpsff1o  17530  dmaf  18011  cdaf  18012  coapm  18033  0pos  18282  isposi  18284  letsr  18552  sgrp0b  18655  frmdplusg  18781  efmndsgrp  18813  smndex1sgrp  18835  smndex1mnd  18837  symg2bas  19323  pmtrsn  19449  odf  19467  efgsfo  19669  efgrelexlemb  19680  isabli  19726  rngmgpf  20066  mgpf  20157  prdscrngd  20231  xrsmgmdifsgrp  21320  xrs1cmn  21323  cnmgpid  21346  zringnzr  21370  zringunit  21376  zringlpir  21377  zringndrg  21378  pzriprnglem5  21395  pzriprnglem7  21397  pzriprnglem9  21399  pzriprnglem13  21403  zzngim  21462  cnmsgngrp  21488  psgninv  21491  zrhpsgnmhm  21493  retos  21527  refld  21528  rzgrp  21532  pjpm  21617  fntopon  22811  istpsi  22829  cmpfi  23295  indisconn  23305  kqf  23634  fbssfi  23724  zfbas  23783  ptcmplem2  23940  prdstmdd  24011  tsmsfbas  24015  ismeti  24213  prdsxmslem2  24417  cnfldms  24663  cnnrg  24668  tgqioo  24688  xrtgioo  24695  recld2  24703  xrge0gsumle  24722  xrge0tsms  24723  addcnlem  24753  divcnOLD  24757  divcn  24759  abscncf  24794  recncf  24795  imcncf  24796  cjcncf  24797  icopnfhmeo  24841  xrhmeo  24844  cnllycmp  24855  isclmi0  24998  iscvsi  25029  cnstrcvs  25041  cncms  25255  ovolf  25383  ovolre  25426  opnmblALT  25504  dveflem  25883  mdegxrf  25973  iaa  26233  ulmdm  26302  dvradcnv  26330  reeff1o  26357  reefiso  26358  reefgim  26360  recosf1o  26444  efifo  26456  logcn  26556  cxpcn3  26658  resqrtcn  26659  logb1  26679  logbmpt  26698  2logb9irrALT  26708  sqrt2cxp2logb9e3  26709  ressatans  26844  lgamcvg2  26965  lgam1  26974  gam1  26975  efnnfsumcl  27013  efchtdvds  27069  ppiub  27115  lgslem2  27209  lgsfcl2  27214  lgsne0  27246  2lgslem1b  27303  padicabvf  27542  bdayfo  27589  scutf  27724  madef  27764  scutfo  27816  addsf  27889  addsfo  27890  negsf  27958  negsfo  27959  negsf1o  27960  subsfo  27969  0ons  28157  1ons  28158  onsiso  28169  dfn0s2  28224  1nns  28241  bdayn0sf1o  28259  twocut  28309  0reno  28348  istrkg3ld  28388  axlowdimlem16  28884  upgrbi  29020  umgrbi  29028  lfuhgr1v0e  29181  cusgr0  29353  wlk2v2elem2  30085  upgr4cycl4dv4e  30114  konigsberglem4  30184  frgr0  30194  ex-pss  30357  ex-fl  30376  ex-mod  30378  isgrpoi  30427  grporn  30450  isabloi  30480  smcnlem  30626  lnocoi  30686  cncph  30748  cnbn  30798  cnchl  30845  norm3adifii  31077  hhph  31107  hhhl  31133  hlim0  31164  hlimf  31166  helch  31172  hsn0elch  31177  hhssabloilem  31190  hhssnv  31193  hhshsslem2  31197  hhssbnOLD  31208  shscli  31246  shintcli  31258  chintcli  31260  shsval2i  31316  pjhthlem2  31321  lejdii  31467  nonbooli  31580  pjrni  31631  pjfoi  31632  pjfi  31633  pjmf1  31645  df0op2  31681  idunop  31907  0cnop  31908  0cnfn  31909  idcnop  31910  idhmop  31911  0hmop  31912  0lnfn  31914  0bdop  31922  lnophsi  31930  lnopcoi  31932  lnopunii  31941  lnophmi  31947  nmcopex  31958  nmcoplb  31959  nmcfnex  31982  nmcfnlb  31983  imaelshi  31987  nlelshi  31989  nlelchi  31990  riesz4i  31992  riesz4  31993  riesz1  31994  cnlnadjlem6  32001  cnlnadjlem9  32004  cnlnadjeui  32006  cnlnadjeu  32007  nmopadji  32019  bdophsi  32025  bdopcoi  32027  nmopcoadji  32030  pjhmopi  32075  pjbdlni  32078  hmopidmchi  32080  mdslj1i  32248  rinvf1o  32554  nnindf  32744  rpdp2cl  32802  dp2ltc  32807  dpmul4  32834  s3clhash  32869  xrstos  32948  xrsclat  32949  xrge0tsmsd  33002  xrge0omnd  33025  qfld  33247  cnfldfld  33314  reofld  33315  nn0archi  33318  zringidom  33522  zringfrac  33525  ccfldextrr  33642  ccfldsrarelvec  33666  ccfldextdgrr  33667  2sqr3minply  33770  xrge0iifmhm  33929  xrge0pluscn  33930  cnzh  33958  rezh  33959  qqhval2lem  33971  esum0  34039  esumcst  34053  esumpcvgval  34068  esumcvg  34076  dmvlsiga  34119  measdivcstALTV  34215  eulerpartlemt  34362  coinfliprv  34474  ballotlem2  34480  signswmnd  34548  logdivsqrle  34641  hgt750lem  34642  bnj906  34920  indispconn  35221  cnllysconn  35232  rellysconn  35238  msrf  35529  brbigcup  35886  fobigcup  35888  brsingle  35905  fnsingle  35907  brimage  35914  funimage  35916  fnimage  35917  imageval  35918  brcart  35920  brapply  35926  brcup  35927  brcap  35928  funpartfun  35931  brub  35942  mpomulnzcnf  36287  onsucconni  36425  onsucsuccmpi  36431  dnicn  36480  bj-wnfnf  36727  bj-nnfv  36742  bj-nnfa1  36747  bj-nnfe1  36748  bj-rabtr  36918  taupilem2  37310  taupi  37311  f1omptsnlem  37324  icoreresf  37340  relowlpssretop  37352  finxpreclem3  37381  matunitlindf  37612  mblfinlem2  37652  areacirc  37707  0totbnd  37767  heiborlem6  37810  refrelid  38513  idsymrel  38552  trrelressn  38574  refrelsredund4  38623  refrelredund4  38626  disjALTV0  38746  disjALTVid  38747  antisymrelressn  38756  isolatiN  39209  isomliN  39232  ishlatiN  39348  mzpclall  42715  jm2.20nn  42986  dfacbasgrp  43097  dgraaf  43136  onexoegt  43233  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  44296  dvsid  44320  rankrelp  44950  halffl  45294  resincncf  45873  0cnf  45875  iblempty  45963  dirkeritg  46100  fourierdlem62  46166  fourierdlem76  46180  fourierdlem103  46207  etransclem18  46250  etransclem46  46278  abnotbtaxb  46916  dfaiota3  47093  ceilhalf1  47335  sprsymrelf1  47497  fmtnof1  47536  fmtno4prm  47576  prmdvdsfmtnof1  47588  31prm  47598  requad01  47622  0evenALTV  47689  1oddALTV  47691  2evenALTV  47693  6even  47712  8even  47714  6gbe  47772  7gbow  47773  8gbe  47774  9gbo  47775  11gbo  47776  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2trifr  48028  gpg5grlic  48084  uspgrsprf1  48135  1odd  48159  nnsgrp  48165  0even  48225  2even  48227  2zrngamgm  48233  2zrngasgrp  48234  2zrngamnd  48235  2zrngagrp  48237  2zrngmsgrp  48241  zlmodzxzldeplem3  48491  lvecpsslmod  48496  ldepsnlinc  48497  blennngt2o2  48581  blennn0e2  48583  ackval42  48685  rrx2xpref1o  48707  rrx2plordisom  48712  slotresfo  48887  sepfsepc  48916  basresposfo  48966  oppff1  49137  setcsnterm  49479  setc1onsubc  49591  setrec2lem2  49683  aacllem  49790