Theorem mpbir2an 710

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 708	. 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  1339  euequ  2600  eqssi  4025  elini  4222  dtruALT2  5388  exexneq  5454  dtruOLD  5461  opnzi  5494  so0  5645  we0  5695  difxp  6195  ord0  6448  dfiota4  6565  funi  6610  funcnvsn  6628  idfn  6708  fn0  6711  f0  6802  fconst  6807  f10  6895  f1o0  6899  f1oi  6900  f1osn  6902  isoid  7365  porpss  7762  epweon  7810  epweonALT  7811  ordon  7812  omssnlim  7918  peano1  7927  fo1st  8050  fo2nd  8051  soseq  8200  wfrfunOLD  8375  wfr1OLD  8383  iordsmo  8413  tfrlem7  8439  tfr1  8453  frfnom  8491  seqomlem2  8507  oawordeulem  8610  1onn  8696  2onn  8698  naddf  8737  mapsnf1o2  8952  canth2  9196  1sdom2  9303  unfilem2  9372  cantnfvalf  9734  cnfcom3clem  9774  ssttrcl  9784  tc2  9811  r111  9844  rankf  9863  cardf2  10012  harcard  10047  r0weon  10081  infxpenc  10087  infxpenc2lem1  10088  alephon  10138  alephf1  10154  alephiso  10167  alephsmo  10171  alephf1ALT  10172  alephfplem4  10176  ackbij1lem17  10304  ackbij1  10306  ackbij2  10311  fin1a2lem2  10470  fin1a2lem4  10472  axcc2lem  10505  iunfo  10608  smobeth  10655  0tsk  10824  1pi  10952  nqerf  10999  axaddf  11214  axmulf  11215  axicn  11219  mpoaddf  11278  mpomulf  11279  mulnzcnf  11936  negiso  12275  dfnn2  12306  nnind  12311  0z  12650  dfuzi  12734  cnref1o  13050  elrpii  13060  0e0icopnf  13518  0e0iccpnf  13519  fldiv4p1lem1div2  13886  om2uzf1oi  14004  om2uzisoi  14005  uzrdgfni  14009  expcl2lem  14124  expclzlem  14134  expge0  14149  expge1  14150  faclbnd4lem1  14342  hashkf  14381  wwlktovf1  15006  sqrtf  15412  fclim  15599  fprodn0f  16039  eff2  16147  reeff1  16168  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  sin01gt0  16238  egt2lt3  16254  qnnen  16261  ruc  16291  halfleoddlt  16410  divalglem2  16443  divalglem9  16449  bitsf1  16492  sadaddlem  16512  2prm  16739  3prm  16741  1arith  16974  prmlem1a  17154  setsnid  17256  setsnidOLD  17257  xpsff1o  17627  dmaf  18116  cdaf  18117  coapm  18138  0pos  18391  0posOLD  18392  isposi  18394  letsr  18663  sgrp0b  18766  frmdplusg  18889  efmndsgrp  18921  smndex1sgrp  18943  smndex1mnd  18945  symg2bas  19434  pmtrsn  19561  odf  19579  efgsfo  19781  efgrelexlemb  19792  isabli  19838  rngmgpf  20184  mgpf  20275  prdscrngd  20345  xrsmgmdifsgrp  21444  xrs1cmn  21447  cnmgpid  21470  zringnzr  21494  zringunit  21500  zringlpir  21501  zringndrg  21502  pzriprnglem5  21519  pzriprnglem7  21521  pzriprnglem9  21523  pzriprnglem13  21527  zzngim  21594  cnmsgngrp  21620  psgninv  21623  zrhpsgnmhm  21625  retos  21659  refld  21660  rzgrp  21664  pjpm  21751  fntopon  22951  istpsi  22969  cmpfi  23437  indisconn  23447  kqf  23776  fbssfi  23866  zfbas  23925  ptcmplem2  24082  prdstmdd  24153  tsmsfbas  24157  ismeti  24356  prdsxmslem2  24563  cnfldms  24817  cnnrg  24822  tgqioo  24841  xrtgioo  24847  recld2  24855  xrge0gsumle  24874  xrge0tsms  24875  addcnlem  24905  divcnOLD  24909  divcn  24911  abscncf  24946  recncf  24947  imcncf  24948  cjcncf  24949  icopnfhmeo  24993  xrhmeo  24996  cnllycmp  25007  isclmi0  25150  iscvsi  25181  cnstrcvs  25193  cncms  25408  ovolf  25536  ovolre  25579  opnmblALT  25657  dveflem  26037  mdegxrf  26127  iaa  26385  ulmdm  26454  dvradcnv  26482  reeff1o  26509  reefiso  26510  reefgim  26512  recosf1o  26595  efifo  26607  logcn  26707  cxpcn3  26809  resqrtcn  26810  logb1  26830  logbmpt  26849  2logb9irrALT  26859  sqrt2cxp2logb9e3  26860  ressatans  26995  lgamcvg2  27116  lgam1  27125  gam1  27126  efnnfsumcl  27164  efchtdvds  27220  ppiub  27266  lgslem2  27360  lgsfcl2  27365  lgsne0  27397  2lgslem1b  27454  padicabvf  27693  bdayfo  27740  scutf  27875  madef  27913  scutfo  27960  addsf  28033  addsfo  28034  negsf  28102  negsfo  28103  negsf1o  28104  subsfo  28113  0ons  28297  1ons  28298  dfn0s2  28354  1nns  28370  nohalf  28425  0reno  28447  istrkg3ld  28487  axlowdimlem16  28990  upgrbi  29128  umgrbi  29136  lfuhgr1v0e  29289  cusgr0  29461  wlk2v2elem2  30188  upgr4cycl4dv4e  30217  konigsberglem4  30287  frgr0  30297  ex-pss  30460  ex-fl  30479  ex-mod  30481  isgrpoi  30530  grporn  30553  isabloi  30583  smcnlem  30729  lnocoi  30789  cncph  30851  cnbn  30901  cnchl  30948  norm3adifii  31180  hhph  31210  hhhl  31236  hlim0  31267  hlimf  31269  helch  31275  hsn0elch  31280  hhssabloilem  31293  hhssnv  31296  hhshsslem2  31300  hhssbnOLD  31311  shscli  31349  shintcli  31361  chintcli  31363  shsval2i  31419  pjhthlem2  31424  lejdii  31570  nonbooli  31683  pjrni  31734  pjfoi  31735  pjfi  31736  pjmf1  31748  df0op2  31784  idunop  32010  0cnop  32011  0cnfn  32012  idcnop  32013  idhmop  32014  0hmop  32015  0lnfn  32017  0bdop  32025  lnophsi  32033  lnopcoi  32035  lnopunii  32044  lnophmi  32050  nmcopex  32061  nmcoplb  32062  nmcfnex  32085  nmcfnlb  32086  imaelshi  32090  nlelshi  32092  nlelchi  32093  riesz4i  32095  riesz4  32096  riesz1  32097  cnlnadjlem6  32104  cnlnadjlem9  32107  cnlnadjeui  32109  cnlnadjeu  32110  nmopadji  32122  bdophsi  32128  bdopcoi  32130  nmopcoadji  32133  pjhmopi  32178  pjbdlni  32181  hmopidmchi  32183  mdslj1i  32351  rinvf1o  32649  nnindf  32823  rpdp2cl  32846  dp2ltc  32851  dpmul4  32878  s3clhash  32914  xrstos  32993  xrsclat  32994  xrge0tsmsd  33041  xrge0omnd  33061  cnfldfld  33336  reofld  33337  nn0archi  33340  zringidom  33544  zringfrac  33547  ccfldextrr  33661  ccfldsrarelvec  33681  ccfldextdgrr  33682  2sqr3minply  33738  xrge0iifmhm  33885  xrge0pluscn  33886  cnzh  33916  rezh  33917  qqhval2lem  33927  esum0  34013  esumcst  34027  esumpcvgval  34042  esumcvg  34050  dmvlsiga  34093  measdivcstALTV  34189  eulerpartlemt  34336  coinfliprv  34447  ballotlem2  34453  signswmnd  34534  logdivsqrle  34627  hgt750lem  34628  bnj906  34906  indispconn  35202  cnllysconn  35213  rellysconn  35219  msrf  35510  brbigcup  35862  fobigcup  35864  brsingle  35881  fnsingle  35883  brimage  35890  funimage  35892  fnimage  35893  imageval  35894  brcart  35896  brapply  35902  brcup  35903  brcap  35904  funpartfun  35907  brub  35918  mpomulnzcnf  36265  onsucconni  36403  onsucsuccmpi  36409  dnicn  36458  bj-wnfnf  36705  bj-nnfv  36720  bj-nnfa1  36725  bj-nnfe1  36726  bj-rabtr  36896  taupilem2  37288  taupi  37289  f1omptsnlem  37302  icoreresf  37318  relowlpssretop  37330  finxpreclem3  37359  matunitlindf  37578  mblfinlem2  37618  areacirc  37673  0totbnd  37733  heiborlem6  37776  refrelid  38478  idsymrel  38517  trrelressn  38539  refrelsredund4  38588  refrelredund4  38591  disjALTV0  38710  disjALTVid  38711  antisymrelressn  38720  isolatiN  39172  isomliN  39195  ishlatiN  39311  mzpclall  42683  jm2.20nn  42954  dfacbasgrp  43065  dgraaf  43104  onexoegt  43205  omnord1  43267  oege2  43269  oenord1  43278  cantnftermord  43282  cantnf2  43287  omabs2  43294  omcl2  43295  ifpim3  43458  ifpim4  43460  ifpbi1b  43465  eu0  43482  omiscard  43505  iso0  44276  dvsid  44300  halffl  45211  resincncf  45796  0cnf  45798  iblempty  45886  dirkeritg  46023  fourierdlem62  46089  fourierdlem76  46103  fourierdlem103  46130  etransclem18  46173  etransclem46  46201  abnotbtaxb  46830  dfaiota3  47007  sprsymrelf1  47370  fmtnof1  47409  fmtno4prm  47449  prmdvdsfmtnof1  47461  31prm  47471  requad01  47495  0evenALTV  47562  1oddALTV  47564  2evenALTV  47566  6even  47585  8even  47587  6gbe  47645  7gbow  47646  8gbe  47647  9gbo  47648  11gbo  47649  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2trifr  47852  uspgrsprf1  47870  1odd  47894  nnsgrp  47900  0even  47960  2even  47962  2zrngamgm  47968  2zrngasgrp  47969  2zrngamnd  47970  2zrngagrp  47972  2zrngmsgrp  47976  zlmodzxzldeplem3  48231  lvecpsslmod  48236  ldepsnlinc  48237  blennngt2o2  48326  blennn0e2  48328  ackval42  48430  rrx2xpref1o  48452  rrx2plordisom  48457  sepfsepc  48607  setrec2lem2  48786  aacllem  48895