Theorem mpbir2an 712

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 710	. 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  1341  euequ  2598  eqssi  3939  elini  4140  dtruALT2  5307  exexneq  5382  opnzi  5422  so0  5570  we0  5619  difxp  6122  ord0  6371  dfiota4  6484  funi  6524  funcnvsn  6542  idfn  6620  fn0  6623  f0  6715  fconst  6720  f10  6807  f1o0  6811  f1oiOLD  6813  f1osn  6815  isoid  7277  porpss  7674  epweon  7722  epweonALT  7723  ordon  7724  omssnlim  7825  peano1  7833  fo1st  7955  fo2nd  7956  soseq  8102  iordsmo  8290  tfrlem7  8315  tfr1  8329  frfnom  8367  seqomlem2  8383  oawordeulem  8482  1onn  8569  2onn  8571  naddf  8610  mapsnf1o2  8835  canth2  9061  1sdom2  9151  unfilem2  9209  cantnfvalf  9577  cnfcom3clem  9617  ssttrcl  9627  tc2  9652  r111  9690  rankf  9709  cardf2  9858  harcard  9893  r0weon  9925  infxpenc  9931  infxpenc2lem1  9932  alephon  9982  alephf1  9998  alephiso  10011  alephsmo  10015  alephf1ALT  10016  alephfplem4  10020  ackbij1lem17  10148  ackbij1  10150  ackbij2  10155  fin1a2lem2  10314  fin1a2lem4  10316  axcc2lem  10349  iunfo  10452  smobeth  10500  0tsk  10669  1pi  10797  nqerf  10844  axaddf  11059  axmulf  11060  axicn  11064  mpoaddf  11123  mpomulf  11124  mulnzcnf  11787  negiso  12127  dfnn2  12178  nnind  12183  0z  12526  dfuzi  12611  cnref1o  12926  elrpii  12936  0e0icopnf  13402  0e0iccpnf  13403  fldiv4p1lem1div2  13785  om2uzf1oi  13906  om2uzisoi  13907  uzrdgfni  13911  expcl2lem  14026  expclzlem  14036  expge0  14051  expge1  14052  faclbnd4lem1  14246  hashkf  14285  wwlktovf1  14910  sqrtf  15317  fclim  15506  fprodn0f  15947  eff2  16057  reeff1  16078  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  sin01gt0  16148  egt2lt3  16164  qnnen  16171  ruc  16201  halfleoddlt  16322  divalglem2  16355  divalglem9  16361  bitsf1  16406  sadaddlem  16426  2prm  16652  3prm  16654  1arith  16889  prmlem1a  17068  setsnid  17169  xpsff1o  17522  dmaf  18007  cdaf  18008  coapm  18029  0pos  18278  isposi  18280  letsr  18550  ex-chn1  18594  ex-chn2  18595  sgrp0b  18687  frmdplusg  18813  efmndsgrp  18845  smndex1sgrp  18870  smndex1mnd  18872  symg2bas  19359  pmtrsn  19485  odf  19503  efgsfo  19705  efgrelexlemb  19716  isabli  19762  rngmgpf  20129  mgpf  20220  prdscrngd  20292  xrsmgmdifsgrp  21398  cnmgpid  21419  xrs1cmn  21432  xrge0omnd  21435  zringnzr  21450  zringunit  21456  zringlpir  21457  zringndrg  21458  pzriprnglem5  21475  pzriprnglem7  21477  pzriprnglem9  21479  pzriprnglem13  21483  zzngim  21542  cnmsgngrp  21569  psgninv  21572  zrhpsgnmhm  21574  retos  21608  refld  21609  rzgrp  21613  pjpm  21698  fntopon  22899  istpsi  22917  cmpfi  23383  indisconn  23393  kqf  23722  fbssfi  23812  zfbas  23871  ptcmplem2  24028  prdstmdd  24099  tsmsfbas  24103  ismeti  24300  prdsxmslem2  24504  cnfldms  24750  cnnrg  24755  tgqioo  24775  xrtgioo  24782  recld2  24790  xrge0gsumle  24809  xrge0tsms  24810  addcnlem  24840  divcn  24845  abscncf  24878  recncf  24879  imcncf  24880  cjcncf  24881  icopnfhmeo  24920  xrhmeo  24923  cnllycmp  24933  isclmi0  25075  iscvsi  25106  cnstrcvs  25118  cncms  25332  ovolf  25459  ovolre  25502  opnmblALT  25580  dveflem  25956  mdegxrf  26043  iaa  26302  ulmdm  26371  dvradcnv  26399  reeff1o  26425  reefiso  26426  reefgim  26428  recosf1o  26512  efifo  26524  logcn  26624  cxpcn3  26725  resqrtcn  26726  logb1  26746  logbmpt  26765  2logb9irrALT  26775  sqrt2cxp2logb9e3  26776  ressatans  26911  lgamcvg2  27032  lgam1  27041  gam1  27042  efnnfsumcl  27080  efchtdvds  27136  ppiub  27181  lgslem2  27275  lgsfcl2  27280  lgsne0  27312  2lgslem1b  27369  padicabvf  27608  bdayfo  27655  cutsf  27798  madef  27842  cutsfo  27911  addsf  27988  addsfo  27989  negsf  28058  negsfo  28059  negsf1o  28060  subsfo  28071  0ons  28262  1ons  28263  oniso  28277  dfn0s2  28338  1nns  28355  bdayn0sf1o  28376  zsoring  28415  twocut  28429  0reno  28502  1reno  28503  istrkg3ld  28543  axlowdimlem16  29040  upgrbi  29176  umgrbi  29184  lfuhgr1v0e  29337  cusgr0  29509  wlk2v2elem2  30241  upgr4cycl4dv4e  30270  konigsberglem4  30340  frgr0  30350  ex-pss  30513  ex-fl  30532  ex-mod  30534  isgrpoi  30584  grporn  30607  isabloi  30637  smcnlem  30783  lnocoi  30843  cncph  30905  cnbn  30955  cnchl  31002  norm3adifii  31234  hhph  31264  hhhl  31290  hlim0  31321  hlimf  31323  helch  31329  hsn0elch  31334  hhssabloilem  31347  hhssnv  31350  hhshsslem2  31354  hhssbnOLD  31365  shscli  31403  shintcli  31415  chintcli  31417  shsval2i  31473  pjhthlem2  31478  lejdii  31624  nonbooli  31737  pjrni  31788  pjfoi  31789  pjfi  31790  pjmf1  31802  df0op2  31838  idunop  32064  0cnop  32065  0cnfn  32066  idcnop  32067  idhmop  32068  0hmop  32069  0lnfn  32071  0bdop  32079  lnophsi  32087  lnopcoi  32089  lnopunii  32098  lnophmi  32104  nmcopex  32115  nmcoplb  32116  nmcfnex  32139  nmcfnlb  32140  imaelshi  32144  nlelshi  32146  nlelchi  32147  riesz4i  32149  riesz4  32150  riesz1  32151  cnlnadjlem6  32158  cnlnadjlem9  32161  cnlnadjeui  32163  cnlnadjeu  32164  nmopadji  32176  bdophsi  32182  bdopcoi  32184  nmopcoadji  32187  pjhmopi  32232  pjbdlni  32235  hmopidmchi  32237  mdslj1i  32405  rinvf1o  32718  nnindf  32908  rpdp2cl  32956  dp2ltc  32961  dpmul4  32988  s3clhash  33023  xrstos  33085  xrsclat  33086  xrge0tsmsd  33149  qfld  33373  cnfldfld  33417  reofld  33418  nn0archi  33422  zringidom  33626  zringfrac  33629  ccfldextrr  33806  ccfldsrarelvec  33831  ccfldextdgrr  33832  2sqr3minply  33940  xrge0iifmhm  34099  xrge0pluscn  34100  cnzh  34128  rezh  34129  qqhval2lem  34141  esum0  34209  esumcst  34223  esumpcvgval  34238  esumcvg  34246  dmvlsiga  34289  measdivcstALTV  34385  eulerpartlemt  34531  coinfliprv  34643  ballotlem2  34649  signswmnd  34717  logdivsqrle  34810  hgt750lem  34811  bnj906  35088  xoromon  35248  fineqvnttrclse  35284  indispconn  35432  cnllysconn  35443  rellysconn  35449  msrf  35740  brbigcup  36094  fobigcup  36096  brsingle  36113  fnsingle  36115  brimage  36122  funimage  36124  fnimage  36125  imageval  36126  brcart  36128  brapply  36134  brcup  36135  brcap  36136  funpartfun  36141  brub  36152  mpomulnzcnf  36497  onsucconni  36635  onsucsuccmpi  36641  dnicn  36768  bj-nnfv  37081  bj-wnfnf  37096  bj-nnfa1  37097  bj-nnfe1  37098  bj-rabtr  37253  bj-axreprepsep  37398  taupilem2  37652  taupi  37653  f1omptsnlem  37666  icoreresf  37682  relowlpssretop  37694  finxpreclem3  37723  matunitlindf  37953  mblfinlem2  37993  areacirc  38048  0totbnd  38108  heiborlem6  38151  dfsucmap3  38798  refrelid  38937  idsymrel  38980  trrelressn  39002  refrelsredund4  39051  refrelredund4  39054  disjALTV0  39189  disjALTVid  39190  antisymrelressn  39202  isolatiN  39676  isomliN  39699  ishlatiN  39815  mzpclall  43173  jm2.20nn  43443  dfacbasgrp  43554  dgraaf  43593  onexoegt  43690  omnord1  43751  oege2  43753  oenord1  43762  cantnftermord  43766  cantnf2  43771  omabs2  43778  omcl2  43779  ifpim3  43941  ifpim4  43943  ifpbi1b  43948  eu0  43965  omiscard  43988  iso0  44752  dvsid  44776  rankrelp  45405  halffl  45747  resincncf  46321  0cnf  46323  iblempty  46411  dirkeritg  46548  fourierdlem62  46614  fourierdlem76  46628  fourierdlem103  46655  etransclem18  46698  etransclem46  46726  abnotbtaxb  47375  dfaiota3  47552  ceilhalf1  47798  sprsymrelf1  47968  fmtnof1  48010  fmtno4prm  48050  prmdvdsfmtnof1  48062  31prm  48072  requad01  48109  0evenALTV  48176  1oddALTV  48178  2evenALTV  48180  6even  48199  8even  48201  6gbe  48259  7gbow  48260  8gbe  48261  9gbo  48262  11gbo  48263  usgrexmpl1lem  48509  usgrexmpl2lem  48514  usgrexmpl2trifr  48525  gpg5grlim  48581  gpg5grlic  48582  uspgrsprf1  48635  1odd  48659  nnsgrp  48665  0even  48725  2even  48727  2zrngamgm  48733  2zrngasgrp  48734  2zrngamnd  48735  2zrngagrp  48737  2zrngmsgrp  48741  zlmodzxzldeplem3  48990  lvecpsslmod  48995  ldepsnlinc  48996  blennngt2o2  49080  blennn0e2  49082  ackval42  49184  rrx2xpref1o  49206  rrx2plordisom  49211  slotresfo  49386  sepfsepc  49415  basresposfo  49465  oppff1  49635  setcsnterm  49977  setc1onsubc  50089  setrec2lem2  50181  aacllem  50288