Theorem mpbir2an 708

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 706	. 2 ⊢ (𝜑 ↔ 𝜒)
5	1, 4	mpbir 230	1 ⊢ 𝜑

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  3pm3.2i  1338  euequ  2598  eqssi  3938  elini  4128  dtruALT2  5294  dtru  5360  opnzi  5390  so0  5540  we0  5585  difxp  6072  ord0  6322  dfiota4  6429  funi  6473  funcnvsn  6491  idfn  6569  fnresiOLD  6571  fn0  6573  f0  6664  fconst  6669  f10  6758  f1o0  6762  f1oi  6763  f1osn  6765  isoid  7209  porpss  7589  epweon  7634  epweonOLD  7635  ordon  7636  omssnlim  7736  peano1  7744  fo1st  7860  fo2nd  7861  wfrfunOLD  8159  wfr1OLD  8167  iordsmo  8197  tfrlem7  8223  tfr1  8237  frfnom  8275  seqomlem2  8291  oawordeulem  8394  1onn  8479  2onn  8481  mapsnf1o2  8691  canth2  8926  unfilem2  9088  cantnfvalf  9432  cnfcom3clem  9472  ssttrcl  9482  tc2  9509  r111  9542  rankf  9561  cardf2  9710  harcard  9745  r0weon  9777  infxpenc  9783  infxpenc2lem1  9784  alephon  9834  alephf1  9850  alephiso  9863  alephsmo  9867  alephf1ALT  9868  alephfplem4  9872  ackbij1lem17  10001  ackbij1  10003  ackbij2  10008  fin1a2lem2  10166  fin1a2lem4  10168  axcc2lem  10201  iunfo  10304  smobeth  10351  0tsk  10520  1pi  10648  nqerf  10695  axaddf  10910  axmulf  10911  axicn  10915  mulnzcnopr  11630  negiso  11964  dfnn2  11995  nnind  12000  0z  12339  dfuzi  12420  cnref1o  12734  elrpii  12742  0e0icopnf  13199  0e0iccpnf  13200  fz0to4untppr  13368  fldiv4p1lem1div2  13564  om2uzf1oi  13682  om2uzisoi  13683  uzrdgfni  13687  expcl2lem  13803  expclzlem  13815  expge0  13828  expge1  13829  faclbnd4lem1  14016  hashkf  14055  wwlktovf1  14681  sqrtf  15084  fclim  15271  fprodn0f  15710  eff2  15817  reeff1  15838  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  sin01gt0  15908  egt2lt3  15924  qnnen  15931  ruc  15961  halfleoddlt  16080  divalglem2  16113  divalglem9  16119  bitsf1  16162  sadaddlem  16182  2prm  16406  3prm  16408  1arith  16637  prmlem1a  16817  setsnid  16919  setsnidOLD  16920  xpsff1o  17287  dmaf  17773  cdaf  17774  coapm  17795  0pos  18048  0posOLD  18049  isposi  18051  letsr  18320  sgrp0b  18392  frmdplusg  18502  efmndsgrp  18534  smndex1sgrp  18556  smndex1mnd  18558  symg2bas  19009  pmtrsn  19136  odf  19154  efgsfo  19354  efgrelexlemb  19365  isabli  19410  mgpf  19807  prdscrngd  19861  xrsmgmdifsgrp  20644  xrs1cmn  20647  cnmgpid  20669  zringnzr  20691  zringunit  20697  zringlpir  20698  zringndrg  20699  zzngim  20769  cnmsgngrp  20793  psgninv  20796  zrhpsgnmhm  20798  retos  20832  refld  20833  rzgrp  20837  pjpm  20924  fntopon  22082  istpsi  22100  cmpfi  22568  indisconn  22578  kqf  22907  fbssfi  22997  zfbas  23056  ptcmplem2  23213  prdstmdd  23284  tsmsfbas  23288  ismeti  23487  prdsxmslem2  23694  cnfldms  23948  cnnrg  23953  tgqioo  23972  xrtgioo  23978  recld2  23986  xrge0gsumle  24005  xrge0tsms  24006  addcnlem  24036  divcn  24040  abscncf  24073  recncf  24074  imcncf  24075  cjcncf  24076  icopnfhmeo  24115  xrhmeo  24118  cnllycmp  24128  isclmi0  24270  iscvsi  24301  cnstrcvs  24313  cncms  24528  ovolf  24655  ovolre  24698  opnmblALT  24776  dveflem  25152  mdegxrf  25242  iaa  25494  ulmdm  25561  dvradcnv  25589  reeff1o  25615  reefiso  25616  reefgim  25618  recosf1o  25700  efifo  25712  logcn  25811  cxpcn3  25910  resqrtcn  25911  logb1  25928  logbmpt  25947  2logb9irrALT  25957  sqrt2cxp2logb9e3  25958  ressatans  26093  lgamcvg2  26213  lgam1  26222  gam1  26223  efnnfsumcl  26261  efchtdvds  26317  ppiub  26361  lgslem2  26455  lgsfcl2  26460  lgsne0  26492  2lgslem1b  26549  padicabvf  26788  istrkg3ld  26831  axlowdimlem16  27334  upgrbi  27472  umgrbi  27480  lfuhgr1v0e  27630  cusgr0  27802  wlk2v2elem2  28529  upgr4cycl4dv4e  28558  konigsberglem4  28628  frgr0  28638  ex-pss  28801  ex-fl  28820  ex-mod  28822  isgrpoi  28869  grporn  28892  isabloi  28922  smcnlem  29068  lnocoi  29128  cncph  29190  cnbn  29240  cnchl  29287  norm3adifii  29519  hhph  29549  hhhl  29575  hlim0  29606  hlimf  29608  helch  29614  hsn0elch  29619  hhssabloilem  29632  hhssnv  29635  hhshsslem2  29639  hhssbnOLD  29650  shscli  29688  shintcli  29700  chintcli  29702  shsval2i  29758  pjhthlem2  29763  lejdii  29909  nonbooli  30022  pjrni  30073  pjfoi  30074  pjfi  30075  pjmf1  30087  df0op2  30123  idunop  30349  0cnop  30350  0cnfn  30351  idcnop  30352  idhmop  30353  0hmop  30354  0lnfn  30356  0bdop  30364  lnophsi  30372  lnopcoi  30374  lnopunii  30383  lnophmi  30389  nmcopex  30400  nmcoplb  30401  nmcfnex  30424  nmcfnlb  30425  imaelshi  30429  nlelshi  30431  nlelchi  30432  riesz4i  30434  riesz4  30435  riesz1  30436  cnlnadjlem6  30443  cnlnadjlem9  30446  cnlnadjeui  30448  cnlnadjeu  30449  nmopadji  30461  bdophsi  30467  bdopcoi  30469  nmopcoadji  30472  pjhmopi  30517  pjbdlni  30520  hmopidmchi  30522  mdslj1i  30690  rinvf1o  30974  nnindf  31142  rpdp2cl  31165  dp2ltc  31170  dpmul4  31197  s3clhash  31231  xrstos  31297  xrsclat  31298  xrge0tsmsd  31326  xrge0omnd  31346  reofld  31553  nn0archi  31556  ccfldextrr  31732  ccfldsrarelvec  31750  ccfldextdgrr  31751  xrge0iifmhm  31898  xrge0pluscn  31899  cnzh  31929  rezh  31930  qqhval2lem  31940  esum0  32026  esumcst  32040  esumpcvgval  32055  esumcvg  32063  dmvlsiga  32106  measdivcstALTV  32202  eulerpartlemt  32347  coinfliprv  32458  ballotlem2  32464  signswmnd  32545  logdivsqrle  32639  hgt750lem  32640  bnj906  32919  indispconn  33205  cnllysconn  33216  rellysconn  33222  msrf  33513  soseq  33812  bdayfo  33889  scutf  34015  madef  34049  scutfo  34093  brbigcup  34209  fobigcup  34211  brsingle  34228  fnsingle  34230  brimage  34237  funimage  34239  fnimage  34240  imageval  34241  brcart  34243  brapply  34249  brcup  34250  brcap  34251  funpartfun  34254  brub  34265  onsucconni  34635  onsucsuccmpi  34641  dnicn  34681  bj-wnfnf  34930  bj-nnfv  34945  bj-nnfa1  34950  bj-nnfe1  34951  bj-dtru  35008  bj-rabtr  35127  taupilem2  35502  taupi  35503  f1omptsnlem  35516  icoreresf  35532  relowlpssretop  35544  finxpreclem3  35573  matunitlindf  35784  mblfinlem2  35824  areacirc  35879  0totbnd  35940  heiborlem6  35983  refrelid  36646  idsymrel  36682  refrelsredund4  36752  refrelredund4  36755  disjALTV0  36869  disjALTVid  36870  isolatiN  37237  isomliN  37260  ishlatiN  37376  sn-dtru  40195  mzpclall  40556  jm2.20nn  40826  dfacbasgrp  40940  dgraaf  40979  ifpim3  41110  ifpim4  41112  ifpbi1b  41117  eu0  41134  omiscard  41157  iso0  41932  dvsid  41956  halffl  42842  resincncf  43423  0cnf  43425  iblempty  43513  dirkeritg  43650  fourierdlem62  43716  fourierdlem76  43730  fourierdlem103  43757  etransclem18  43800  etransclem46  43828  abnotbtaxb  44421  dfaiota3  44595  sprsymrelf1  44959  fmtnof1  44998  fmtno4prm  45038  prmdvdsfmtnof1  45050  31prm  45060  requad01  45084  0evenALTV  45151  1oddALTV  45153  2evenALTV  45155  6even  45174  8even  45176  6gbe  45234  7gbow  45235  8gbe  45236  9gbo  45237  11gbo  45238  uspgrsprf1  45320  1odd  45376  nnsgrp  45382  0even  45500  2even  45502  2zrngamgm  45508  2zrngasgrp  45509  2zrngamnd  45510  2zrngagrp  45512  2zrngmsgrp  45516  zlmodzxzldeplem3  45854  lvecpsslmod  45859  ldepsnlinc  45860  blennngt2o2  45949  blennn0e2  45951  ackval42  46053  rrx2xpref1o  46075  rrx2plordisom  46080  sepfsepc  46232  setrec2lem2  46411  aacllem  46516