Theorem mpbir2an 724

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3pm3.2i  1358  euequ  2623  eqssi  3947  elini  4145  dtruALT2  5332  exexneq  5403  opnzi  5443  so0  5597  we0  5646  difxp  6154  ord0  6410  dfiota4  6523  funi  6564  funcnvsn  6582  idfn  6659  fn0  6662  f0  6755  fconst  6760  f10  6850  f1o0  6854  f1oiOLD  6856  f1osn  6858  isoid  7329  porpss  7732  epweon  7778  epweonALT  7779  ordon  7780  omssnlim  7881  peano1  7889  fo1st  8010  fo2nd  8011  soseq  8160  iordsmo  8349  tfrlem7  8375  tfr1  8389  frfnom  8427  seqomlem2  8445  oawordeulem  8546  1onn  8633  2onn  8635  naddf  8675  mapsnf1o2  8906  canth2  9133  1sdom2  9223  unfilem2  9282  cantnfvalf  9650  cnfcom3clem  9690  ssttrcl  9700  tc2  9725  r111  9765  rankf  9784  setrec2lem2  9957  cardf2  10005  harcard  10040  r0weon  10072  infxpenc  10078  infxpenc2lem1  10079  alephon  10129  alephf1  10145  alephiso  10158  alephsmo  10162  alephf1ALT  10163  alephfplem4  10167  ackbij1lem17  10294  ackbij1  10296  ackbij2  10301  fin1a2lem2  10460  fin1a2lem4  10462  axcc2lem  10495  iunfo  10604  smobeth  10652  0tsk  10821  1pi  10949  nqerf  10996  axaddf  11211  axmulf  11212  axicn  11216  mpoaddf  11275  mpomulf  11276  mulnzcnf  11943  negiso  12278  dfnn2  12329  nnind  12334  0z  12685  dfuzi  12771  cnref1o  13094  elrpii  13104  0e0icopnf  13570  0e0iccpnf  13571  fldiv4p1lem1div2  13955  om2uzf1oi  14076  om2uzisoi  14077  uzrdgfni  14081  expcl2lem  14196  expclzlem  14206  expge0  14221  expge1  14222  faclbnd4lem1  14417  hashkf  14456  wwlktovf1  15090  sgnfo  15232  sqrtf  15511  fclim  15700  fprodn0f  16138  eff2  16247  reeff1  16268  ef01bndlem  16332  sin01bnd  16333  cos01bnd  16334  sin01gt0  16338  egt2lt3  16354  qnnen  16361  ruc  16391  halfleoddlt  16512  divalglem2  16545  divalglem9  16551  bitsf1  16596  sadaddlem  16616  2prm  16847  3prm  16849  1arith  17085  prmlem1a  17264  setsnid  17366  xpsff1o  17719  dmaf  18204  cdaf  18205  coapm  18226  0pos  18475  isposi  18477  letsr  18747  ex-chn1  18791  ex-chn2  18792  sgrp0b  18897  frmdplusg  19030  efmndsgrp  19062  smndex1sgrp  19087  smndex1mnd  19089  symg2bas  19587  pmtrsn  19713  odf  19731  efgsfo  19933  efgrelexlemb  19944  isabli  19990  rngmgpf  20359  mgpf  20455  prdscrngd  20531  xrsmgmdifsgrp  21695  cnmgpid  21715  xrs1cmn  21728  xrge0omnd  21731  zringnzr  21746  zringunit  21752  zringlpir  21753  zringndrg  21754  pzriprnglem5  21771  pzriprnglem7  21773  pzriprnglem9  21775  pzriprnglem13  21779  zzngim  21838  cnmsgngrp  21865  psgninv  21868  zrhpsgnmhm  21870  retos  21904  refld  21905  rzgrp  21909  pjpm  21994  matunitlindf  22976  fntopon  23222  istpsi  23240  cmpfi  23706  indisconn  23716  kqf  24046  fbssfi  24136  zfbas  24195  ptcmplem2  24352  prdstmdd  24423  tsmsfbas  24427  ismeti  24624  prdsxmslem2  24828  cnfldms  25074  cnnrg  25079  tgqioo  25099  xrtgioo  25106  recld2  25114  xrge0gsumle  25133  xrge0tsms  25134  addcnlem  25164  divcn  25169  abscncf  25202  recncf  25203  imcncf  25204  cjcncf  25205  icopnfhmeo  25244  xrhmeo  25247  cnllycmp  25257  isclmi0  25399  iscvsi  25430  cnstrcvs  25442  cncms  25656  ovolf  25783  ovolre  25826  opnmblALT  25904  dveflem  26279  mdegxrf  26366  iaaOLD  26634  ulmdm  26702  dvradcnv  26730  reeff1o  26756  reefiso  26757  reefgim  26759  recosf1o  26845  efifo  26857  logcn  26957  cxpcn3  27058  resqrtcn  27059  logb1  27079  logbmpt  27098  2logb9irrALT  27108  sqrt2cxp2logb9e3  27109  ressatans  27244  lgamcvg2  27364  lgam1  27373  gam1  27374  efnnfsumcl  27412  efchtdvds  27468  ppiub  27513  lgslem2  27607  lgsfcl2  27612  lgsne0  27644  2lgslem1b  27701  padicabvf  27940  bdayfo  28016  cutsf  28160  madef  28204  cutsfo  28273  addsf  28350  addsfo  28351  negsf  28420  negsfo  28421  negsf1o  28422  subsfo  28433  0ons  28624  1ons  28625  oniso  28639  dfn0s2  28700  1nns  28717  bdayn0sf1o  28738  zsoring  28777  twocut  28791  0reno  28864  1reno  28865  istrkg3ld  28905  axlowdimlem16  29517  upgrbi  29653  umgrbi  29661  lfuhgr1v0e  29817  cusgr0  29989  wlk2v2elem2  30739  upgr4cycl4dv4e  30768  konigsberglem4  30838  frgr0  30848  ex-pss  31011  ex-fl  31030  ex-mod  31032  isgrpoi  31082  grporn  31105  isabloi  31135  smcnlem  31281  lnocoi  31341  cncph  31403  cnbn  31453  cnchl  31500  norm3adifii  31732  hhph  31762  hhhl  31788  hlim0  31819  hlimf  31821  helch  31827  hsn0elch  31832  hhssabloilem  31845  hhssnv  31848  hhshsslem2  31852  hhssbnOLD  31863  shscli  31901  shintcli  31913  chintcli  31915  shsval2i  31971  pjhthlem2  31976  lejdii  32122  nonbooli  32235  pjrni  32286  pjfoi  32287  pjfi  32288  pjmf1  32300  df0op2  32336  idunop  32562  0cnop  32563  0cnfn  32564  idcnop  32565  idhmop  32566  0hmop  32567  0lnfn  32569  0bdop  32577  lnophsi  32585  lnopcoi  32587  lnopunii  32596  lnophmi  32602  nmcopex  32613  nmcoplb  32614  nmcfnex  32637  nmcfnlb  32638  imaelshi  32642  nlelshi  32644  nlelchi  32645  riesz4i  32647  riesz4  32648  riesz1  32649  cnlnadjlem6  32656  cnlnadjlem9  32659  cnlnadjeui  32661  cnlnadjeu  32662  nmopadji  32674  bdophsi  32680  bdopcoi  32682  nmopcoadji  32685  pjhmopi  32730  pjbdlni  32733  hmopidmchi  32735  mdslj1i  32903  rinvf1o  33206  nnindf  33393  rpdp2cl  33430  dp2ltc  33435  dpmul4  33462  s3clhash  33494  xrstos  33553  xrsclat  33554  xrge0tsmsd  33616  qfld  33841  cnfldfld  33885  reofld  33886  nn0archi  33890  zringidom  34065  zringfrac  34068  ccfldextrr  34260  ccfldsrarelvec  34285  ccfldextdgrr  34286  2sqr3minply  34394  xrge0iifmhm  34553  xrge0pluscn  34554  cnzh  34582  rezh  34583  qqhval2lem  34595  esum0  34663  esumcst  34677  esumpcvgval  34692  esumcvg  34700  dmvlsiga  34743  measdivcstALTV  34840  eulerpartlemt  34986  coinfliprv  35098  ballotlem2  35104  signswmnd  35169  logdivsqrle  35262  hgt750lem  35263  bnj906  35543  xoromon  35697  rankfo  35714  fineqvnttrclse  35765  indispconn  35968  cnllysconn  35979  rellysconn  35985  msrf  36276  brbigcup  36630  fobigcup  36632  brsingle  36649  fnsingle  36651  brimage  36658  funimage  36660  fnimage  36661  imageval  36662  brcart  36664  brapply  36670  brcup  36671  brcap  36672  funpartfun  36677  brub  36688  mpomulnzcnf  37058  onsucconni  37195  onsucsuccmpi  37201  dnicn  37328  bj-nnfv  37640  bj-wnfnf  37655  bj-nnfa1  37656  bj-nnfe1  37657  bj-rabtr  37813  bj-axreprepsep  37959  taupilem2  38211  taupi  38212  f1omptsnlem  38227  icoreresf  38243  relowlpssretop  38255  finxpreclem3  38284  mblfinlem2  38544  areacirc  38599  0totbnd  38675  heiborlem6  38718  dfsucmap3  39363  refrelid  39502  idsymrel  39545  trrelressn  39567  refrelsredund4  39616  refrelredund4  39619  disjALTV0  39754  disjALTVid  39755  antisymrelressn  39767  isolatiN  40241  isomliN  40264  ishlatiN  40380  mzpclall  43691  jm2.20nn  43957  dfacbasgrp  44068  dgraaf  44107  onexoegt  44204  omnord1  44265  oege2  44267  oenord1  44276  cantnftermord  44280  cantnf2  44285  omabs2  44292  omcl2  44293  ifpim3  44455  ifpim4  44457  ifpbi1b  44462  eu0  44479  omiscard  44502  iso0  45250  dvsid  45274  rankrelp  45902  hashomiso  45967  halffl  46255  resincncf  46829  0cnf  46831  iblempty  46919  dirkeritg  47056  fourierdlem62  47122  fourierdlem76  47136  fourierdlem103  47163  etransclem18  47206  etransclem46  47234  sinnpoly  47885  abnotbtaxb  47929  dfaiota3  48106  ceilhalf1  48352  sprsymrelf1  48522  fmtnof1  48564  fmtno4prm  48604  prmdvdsfmtnof1  48616  31prm  48626  requad01  48663  0evenALTV  48730  1oddALTV  48732  2evenALTV  48734  6even  48753  8even  48755  6gbe  48813  7gbow  48814  8gbe  48815  9gbo  48816  11gbo  48817  usgrexmpl1lem  49063  usgrexmpl2lem  49068  usgrexmpl2trifr  49079  gpg5grlim  49135  gpg5grlic  49136  uspgrsprf1  49189  1odd  49212  nnsgrp  49218  0even  49278  2even  49280  2zrngamgm  49286  2zrngasgrp  49287  2zrngamnd  49288  2zrngagrp  49290  2zrngmsgrp  49294  zlmodzxzldeplem3  49558  lvecpsslmod  49563  ldepsnlinc  49564  blennngt2o2  49648  blennn0e2  49650  ackval42  49752  rrx2xpref1o  49774  rrx2plordisom  49779  slotresfo  49951  sepfsepc  49980  basresposfo  50030  oppff1  50200  setcsnterm  50542  setc1onsubc  50654  aacllem  50883  veroquadmodzerod  50928  veroquadnolindfd  50929