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 230	1 ⊢ 𝜑

Syntax hints:   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3pm3.2i  1340  euequ  2592  eqssi  3999  elini  4194  dtruALT2  5369  exexneq  5435  dtruOLD  5442  opnzi  5475  so0  5625  we0  5672  difxp  6164  ord0  6418  dfiota4  6536  funi  6581  funcnvsn  6599  idfn  6679  fn0  6682  f0  6773  fconst  6778  f10  6867  f1o0  6871  f1oi  6872  f1osn  6874  isoid  7326  porpss  7717  epweon  7762  epweonALT  7763  ordon  7764  omssnlim  7870  peano1  7879  fo1st  7995  fo2nd  7996  soseq  8145  wfrfunOLD  8319  wfr1OLD  8327  iordsmo  8357  tfrlem7  8383  tfr1  8397  frfnom  8435  seqomlem2  8451  oawordeulem  8554  1onn  8639  2onn  8641  naddf  8680  mapsnf1o2  8888  canth2  9130  1sdom2  9240  unfilem2  9311  cantnfvalf  9660  cnfcom3clem  9700  ssttrcl  9710  tc2  9737  r111  9770  rankf  9789  cardf2  9938  harcard  9973  r0weon  10007  infxpenc  10013  infxpenc2lem1  10014  alephon  10064  alephf1  10080  alephiso  10093  alephsmo  10097  alephf1ALT  10098  alephfplem4  10102  ackbij1lem17  10231  ackbij1  10233  ackbij2  10238  fin1a2lem2  10396  fin1a2lem4  10398  axcc2lem  10431  iunfo  10534  smobeth  10581  0tsk  10750  1pi  10878  nqerf  10925  axaddf  11140  axmulf  11141  axicn  11145  mulnzcnopr  11860  negiso  12194  dfnn2  12225  nnind  12230  0z  12569  dfuzi  12653  cnref1o  12969  elrpii  12977  0e0icopnf  13435  0e0iccpnf  13436  fz0to4untppr  13604  fldiv4p1lem1div2  13800  om2uzf1oi  13918  om2uzisoi  13919  uzrdgfni  13923  expcl2lem  14039  expclzlem  14049  expge0  14064  expge1  14065  faclbnd4lem1  14253  hashkf  14292  wwlktovf1  14908  sqrtf  15310  fclim  15497  fprodn0f  15935  eff2  16042  reeff1  16063  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  sin01gt0  16133  egt2lt3  16149  qnnen  16156  ruc  16186  halfleoddlt  16305  divalglem2  16338  divalglem9  16344  bitsf1  16387  sadaddlem  16407  2prm  16629  3prm  16631  1arith  16860  prmlem1a  17040  setsnid  17142  setsnidOLD  17143  xpsff1o  17513  dmaf  17999  cdaf  18000  coapm  18021  0pos  18274  0posOLD  18275  isposi  18277  letsr  18546  sgrp0b  18619  frmdplusg  18735  efmndsgrp  18767  smndex1sgrp  18789  smndex1mnd  18791  symg2bas  19260  pmtrsn  19387  odf  19405  efgsfo  19607  efgrelexlemb  19618  isabli  19664  mgpf  20071  prdscrngd  20135  xrsmgmdifsgrp  20982  xrs1cmn  20985  cnmgpid  21007  zringnzr  21030  zringunit  21036  zringlpir  21037  zringndrg  21038  zzngim  21108  cnmsgngrp  21132  psgninv  21135  zrhpsgnmhm  21137  retos  21171  refld  21172  rzgrp  21176  pjpm  21263  fntopon  22426  istpsi  22444  cmpfi  22912  indisconn  22922  kqf  23251  fbssfi  23341  zfbas  23400  ptcmplem2  23557  prdstmdd  23628  tsmsfbas  23632  ismeti  23831  prdsxmslem2  24038  cnfldms  24292  cnnrg  24297  tgqioo  24316  xrtgioo  24322  recld2  24330  xrge0gsumle  24349  xrge0tsms  24350  addcnlem  24380  divcn  24384  abscncf  24417  recncf  24418  imcncf  24419  cjcncf  24420  icopnfhmeo  24459  xrhmeo  24462  cnllycmp  24472  isclmi0  24614  iscvsi  24645  cnstrcvs  24657  cncms  24872  ovolf  24999  ovolre  25042  opnmblALT  25120  dveflem  25496  mdegxrf  25586  iaa  25838  ulmdm  25905  dvradcnv  25933  reeff1o  25959  reefiso  25960  reefgim  25962  recosf1o  26044  efifo  26056  logcn  26155  cxpcn3  26256  resqrtcn  26257  logb1  26274  logbmpt  26293  2logb9irrALT  26303  sqrt2cxp2logb9e3  26304  ressatans  26439  lgamcvg2  26559  lgam1  26568  gam1  26569  efnnfsumcl  26607  efchtdvds  26663  ppiub  26707  lgslem2  26801  lgsfcl2  26806  lgsne0  26838  2lgslem1b  26895  padicabvf  27134  bdayfo  27180  scutf  27313  madef  27351  scutfo  27398  addsf  27466  addsfo  27467  negsf  27526  negsfo  27527  negsf1o  27528  istrkg3ld  27712  axlowdimlem16  28215  upgrbi  28353  umgrbi  28361  lfuhgr1v0e  28511  cusgr0  28683  wlk2v2elem2  29409  upgr4cycl4dv4e  29438  konigsberglem4  29508  frgr0  29518  ex-pss  29681  ex-fl  29700  ex-mod  29702  isgrpoi  29751  grporn  29774  isabloi  29804  smcnlem  29950  lnocoi  30010  cncph  30072  cnbn  30122  cnchl  30169  norm3adifii  30401  hhph  30431  hhhl  30457  hlim0  30488  hlimf  30490  helch  30496  hsn0elch  30501  hhssabloilem  30514  hhssnv  30517  hhshsslem2  30521  hhssbnOLD  30532  shscli  30570  shintcli  30582  chintcli  30584  shsval2i  30640  pjhthlem2  30645  lejdii  30791  nonbooli  30904  pjrni  30955  pjfoi  30956  pjfi  30957  pjmf1  30969  df0op2  31005  idunop  31231  0cnop  31232  0cnfn  31233  idcnop  31234  idhmop  31235  0hmop  31236  0lnfn  31238  0bdop  31246  lnophsi  31254  lnopcoi  31256  lnopunii  31265  lnophmi  31271  nmcopex  31282  nmcoplb  31283  nmcfnex  31306  nmcfnlb  31307  imaelshi  31311  nlelshi  31313  nlelchi  31314  riesz4i  31316  riesz4  31317  riesz1  31318  cnlnadjlem6  31325  cnlnadjlem9  31328  cnlnadjeui  31330  cnlnadjeu  31331  nmopadji  31343  bdophsi  31349  bdopcoi  31351  nmopcoadji  31354  pjhmopi  31399  pjbdlni  31402  hmopidmchi  31404  mdslj1i  31572  rinvf1o  31854  nnindf  32025  rpdp2cl  32048  dp2ltc  32053  dpmul4  32080  s3clhash  32114  xrstos  32180  xrsclat  32181  xrge0tsmsd  32209  xrge0omnd  32229  reofld  32459  nn0archi  32462  ccfldextrr  32727  ccfldsrarelvec  32745  ccfldextdgrr  32746  xrge0iifmhm  32919  xrge0pluscn  32920  cnzh  32950  rezh  32951  qqhval2lem  32961  esum0  33047  esumcst  33061  esumpcvgval  33076  esumcvg  33084  dmvlsiga  33127  measdivcstALTV  33223  eulerpartlemt  33370  coinfliprv  33481  ballotlem2  33487  signswmnd  33568  logdivsqrle  33662  hgt750lem  33663  bnj906  33941  indispconn  34225  cnllysconn  34236  rellysconn  34242  msrf  34533  brbigcup  34870  fobigcup  34872  brsingle  34889  fnsingle  34891  brimage  34898  funimage  34900  fnimage  34901  imageval  34902  brcart  34904  brapply  34910  brcup  34911  brcap  34912  funpartfun  34915  brub  34926  mpomulf  35159  gg-divcn  35163  onsucconni  35322  onsucsuccmpi  35328  dnicn  35368  bj-wnfnf  35617  bj-nnfv  35632  bj-nnfa1  35637  bj-nnfe1  35638  bj-rabtr  35810  taupilem2  36203  taupi  36204  f1omptsnlem  36217  icoreresf  36233  relowlpssretop  36245  finxpreclem3  36274  matunitlindf  36486  mblfinlem2  36526  areacirc  36581  0totbnd  36641  heiborlem6  36684  refrelid  37392  idsymrel  37431  trrelressn  37453  refrelsredund4  37502  refrelredund4  37505  disjALTV0  37624  disjALTVid  37625  antisymrelressn  37634  isolatiN  38086  isomliN  38109  ishlatiN  38225  mzpclall  41465  jm2.20nn  41736  dfacbasgrp  41850  dgraaf  41889  onexoegt  41993  omnord1  42055  oege2  42057  oenord1  42066  cantnftermord  42070  cantnf2  42075  omabs2  42082  omcl2  42083  ifpim3  42247  ifpim4  42249  ifpbi1b  42254  eu0  42271  omiscard  42294  iso0  43066  dvsid  43090  halffl  44006  resincncf  44591  0cnf  44593  iblempty  44681  dirkeritg  44818  fourierdlem62  44884  fourierdlem76  44898  fourierdlem103  44925  etransclem18  44968  etransclem46  44996  abnotbtaxb  45625  dfaiota3  45800  sprsymrelf1  46164  fmtnof1  46203  fmtno4prm  46243  prmdvdsfmtnof1  46255  31prm  46265  requad01  46289  0evenALTV  46356  1oddALTV  46358  2evenALTV  46360  6even  46379  8even  46381  6gbe  46439  7gbow  46440  8gbe  46441  9gbo  46442  11gbo  46443  uspgrsprf1  46525  1odd  46581  nnsgrp  46587  rngmgpf  46653  pzriprnglem5  46809  pzriprnglem7  46811  pzriprnglem9  46813  pzriprnglem13  46817  0even  46829  2even  46831  2zrngamgm  46837  2zrngasgrp  46838  2zrngamnd  46839  2zrngagrp  46841  2zrngmsgrp  46845  zlmodzxzldeplem3  47183  lvecpsslmod  47188  ldepsnlinc  47189  blennngt2o2  47278  blennn0e2  47280  ackval42  47382  rrx2xpref1o  47404  rrx2plordisom  47409  sepfsepc  47560  setrec2lem2  47739  aacllem  47848