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  2624  eqssi  3950  elini  4148  dtruALT2  5339  exexneq  5414  opnzi  5454  so0  5605  we0  5654  difxp  6160  ord0  6416  dfiota4  6529  funi  6569  funcnvsn  6587  idfn  6664  fn0  6667  f0  6760  fconst  6765  f10  6855  f1o0  6859  f1oiOLD  6861  f1osn  6863  isoid  7334  porpss  7732  epweon  7778  epweonALT  7779  ordon  7780  omssnlim  7881  peano1  7889  fo1st  8010  fo2nd  8011  soseq  8161  iordsmo  8350  tfrlem7  8376  tfr1  8390  frfnom  8428  seqomlem2  8444  oawordeulem  8545  1onn  8632  2onn  8634  naddf  8674  mapsnf1o2  8905  canth2  9132  1sdom2  9222  unfilem2  9280  cantnfvalf  9648  cnfcom3clem  9688  ssttrcl  9698  tc2  9723  r111  9761  rankf  9780  cardf2  9952  harcard  9987  r0weon  10019  infxpenc  10025  infxpenc2lem1  10026  alephon  10076  alephf1  10092  alephiso  10105  alephsmo  10109  alephf1ALT  10110  alephfplem4  10114  ackbij1lem17  10241  ackbij1  10243  ackbij2  10248  fin1a2lem2  10407  fin1a2lem4  10409  axcc2lem  10442  iunfo  10551  smobeth  10599  0tsk  10768  1pi  10896  nqerf  10943  axaddf  11158  axmulf  11159  axicn  11163  mpoaddf  11222  mpomulf  11223  mulnzcnf  11888  negiso  12223  dfnn2  12274  nnind  12279  0z  12630  dfuzi  12716  cnref1o  13039  elrpii  13049  0e0icopnf  13515  0e0iccpnf  13516  fldiv4p1lem1div2  13900  om2uzf1oi  14021  om2uzisoi  14022  uzrdgfni  14026  expcl2lem  14141  expclzlem  14151  expge0  14166  expge1  14167  faclbnd4lem1  14361  hashkf  14400  wwlktovf1  15034  sgnfo  15176  sqrtf  15455  fclim  15644  fprodn0f  16084  eff2  16193  reeff1  16214  ef01bndlem  16278  sin01bnd  16279  cos01bnd  16280  sin01gt0  16284  egt2lt3  16300  qnnen  16307  ruc  16337  halfleoddlt  16458  divalglem2  16491  divalglem9  16497  bitsf1  16542  sadaddlem  16562  2prm  16788  3prm  16790  1arith  17025  prmlem1a  17204  setsnid  17306  xpsff1o  17659  dmaf  18144  cdaf  18145  coapm  18166  0pos  18415  isposi  18417  letsr  18687  ex-chn1  18731  ex-chn2  18732  sgrp0b  18836  frmdplusg  18969  efmndsgrp  19001  smndex1sgrp  19026  smndex1mnd  19028  symg2bas  19526  pmtrsn  19652  odf  19670  efgsfo  19872  efgrelexlemb  19883  isabli  19929  rngmgpf  20298  mgpf  20393  prdscrngd  20468  xrsmgmdifsgrp  21628  cnmgpid  21648  xrs1cmn  21661  xrge0omnd  21664  zringnzr  21679  zringunit  21685  zringlpir  21686  zringndrg  21687  pzriprnglem5  21704  pzriprnglem7  21706  pzriprnglem9  21708  pzriprnglem13  21712  zzngim  21771  cnmsgngrp  21798  psgninv  21801  zrhpsgnmhm  21803  retos  21837  refld  21838  rzgrp  21842  pjpm  21927  matunitlindf  22909  fntopon  23155  istpsi  23173  cmpfi  23639  indisconn  23649  kqf  23979  fbssfi  24069  zfbas  24128  ptcmplem2  24285  prdstmdd  24356  tsmsfbas  24360  ismeti  24557  prdsxmslem2  24761  cnfldms  25007  cnnrg  25012  tgqioo  25032  xrtgioo  25039  recld2  25047  xrge0gsumle  25066  xrge0tsms  25067  addcnlem  25097  divcn  25102  abscncf  25135  recncf  25136  imcncf  25137  cjcncf  25138  icopnfhmeo  25177  xrhmeo  25180  cnllycmp  25190  isclmi0  25332  iscvsi  25363  cnstrcvs  25375  cncms  25589  ovolf  25716  ovolre  25759  opnmblALT  25837  dveflem  26213  mdegxrf  26300  iaaOLD  26568  ulmdm  26636  dvradcnv  26664  reeff1o  26690  reefiso  26691  reefgim  26693  recosf1o  26780  efifo  26792  logcn  26892  cxpcn3  26993  resqrtcn  26994  logb1  27014  logbmpt  27033  2logb9irrALT  27043  sqrt2cxp2logb9e3  27044  ressatans  27179  lgamcvg2  27299  lgam1  27308  gam1  27309  efnnfsumcl  27347  efchtdvds  27403  ppiub  27448  lgslem2  27542  lgsfcl2  27547  lgsne0  27579  2lgslem1b  27636  padicabvf  27875  bdayfo  27921  cutsf  28065  madef  28109  cutsfo  28178  addsf  28255  addsfo  28256  negsf  28325  negsfo  28326  negsf1o  28327  subsfo  28338  0ons  28529  1ons  28530  oniso  28544  dfn0s2  28605  1nns  28622  bdayn0sf1o  28643  zsoring  28682  twocut  28696  0reno  28769  1reno  28770  istrkg3ld  28810  axlowdimlem16  29422  upgrbi  29558  umgrbi  29566  lfuhgr1v0e  29722  cusgr0  29894  wlk2v2elem2  30644  upgr4cycl4dv4e  30673  konigsberglem4  30743  frgr0  30753  ex-pss  30916  ex-fl  30935  ex-mod  30937  isgrpoi  30987  grporn  31010  isabloi  31040  smcnlem  31186  lnocoi  31246  cncph  31308  cnbn  31358  cnchl  31405  norm3adifii  31637  hhph  31667  hhhl  31693  hlim0  31724  hlimf  31726  helch  31732  hsn0elch  31737  hhssabloilem  31750  hhssnv  31753  hhshsslem2  31757  hhssbnOLD  31768  shscli  31806  shintcli  31818  chintcli  31820  shsval2i  31876  pjhthlem2  31881  lejdii  32027  nonbooli  32140  pjrni  32191  pjfoi  32192  pjfi  32193  pjmf1  32205  df0op2  32241  idunop  32467  0cnop  32468  0cnfn  32469  idcnop  32470  idhmop  32471  0hmop  32472  0lnfn  32474  0bdop  32482  lnophsi  32490  lnopcoi  32492  lnopunii  32501  lnophmi  32507  nmcopex  32518  nmcoplb  32519  nmcfnex  32542  nmcfnlb  32543  imaelshi  32547  nlelshi  32549  nlelchi  32550  riesz4i  32552  riesz4  32553  riesz1  32554  cnlnadjlem6  32561  cnlnadjlem9  32564  cnlnadjeui  32566  cnlnadjeu  32567  nmopadji  32579  bdophsi  32585  bdopcoi  32587  nmopcoadji  32590  pjhmopi  32635  pjbdlni  32638  hmopidmchi  32640  mdslj1i  32808  rinvf1o  33111  nnindf  33298  rpdp2cl  33335  dp2ltc  33340  dpmul4  33367  s3clhash  33399  xrstos  33458  xrsclat  33459  xrge0tsmsd  33521  qfld  33746  cnfldfld  33790  reofld  33791  nn0archi  33795  zringidom  33969  zringfrac  33972  ccfldextrr  34164  ccfldsrarelvec  34189  ccfldextdgrr  34190  2sqr3minply  34298  xrge0iifmhm  34457  xrge0pluscn  34458  cnzh  34486  rezh  34487  qqhval2lem  34499  esum0  34567  esumcst  34581  esumpcvgval  34596  esumcvg  34604  dmvlsiga  34647  measdivcstALTV  34744  eulerpartlemt  34890  coinfliprv  35002  ballotlem2  35008  signswmnd  35073  logdivsqrle  35166  hgt750lem  35167  bnj906  35447  xoromon  35601  rankfo  35627  fineqvnttrclse  35658  indispconn  35821  cnllysconn  35832  rellysconn  35838  msrf  36129  brbigcup  36483  fobigcup  36485  brsingle  36502  fnsingle  36504  brimage  36511  funimage  36513  fnimage  36514  imageval  36515  brcart  36517  brapply  36523  brcup  36524  brcap  36525  funpartfun  36530  brub  36541  mpomulnzcnf  36927  onsucconni  37064  onsucsuccmpi  37070  dnicn  37197  bj-nnfv  37509  bj-wnfnf  37524  bj-nnfa1  37525  bj-nnfe1  37526  bj-rabtr  37682  bj-axreprepsep  37828  taupilem2  38082  taupi  38083  f1omptsnlem  38098  icoreresf  38114  relowlpssretop  38126  finxpreclem3  38155  mblfinlem2  38415  areacirc  38470  0totbnd  38531  heiborlem6  38574  dfsucmap3  39219  refrelid  39358  idsymrel  39401  trrelressn  39423  refrelsredund4  39472  refrelredund4  39475  disjALTV0  39610  disjALTVid  39611  antisymrelressn  39623  isolatiN  40097  isomliN  40120  ishlatiN  40236  mzpclall  43580  jm2.20nn  43846  dfacbasgrp  43957  dgraaf  43996  onexoegt  44093  omnord1  44154  oege2  44156  oenord1  44165  cantnftermord  44169  cantnf2  44174  omabs2  44181  omcl2  44182  ifpim3  44344  ifpim4  44346  ifpbi1b  44351  eu0  44368  omiscard  44391  iso0  45139  dvsid  45163  rankrelp  45791  hashomiso  45856  halffl  46137  resincncf  46711  0cnf  46713  iblempty  46801  dirkeritg  46938  fourierdlem62  47004  fourierdlem76  47018  fourierdlem103  47045  etransclem18  47088  etransclem46  47116  sinnpoly  47767  abnotbtaxb  47811  dfaiota3  47988  ceilhalf1  48234  sprsymrelf1  48404  fmtnof1  48446  fmtno4prm  48486  prmdvdsfmtnof1  48498  31prm  48508  requad01  48545  0evenALTV  48612  1oddALTV  48614  2evenALTV  48616  6even  48635  8even  48637  6gbe  48695  7gbow  48696  8gbe  48697  9gbo  48698  11gbo  48699  usgrexmpl1lem  48945  usgrexmpl2lem  48950  usgrexmpl2trifr  48961  gpg5grlim  49017  gpg5grlic  49018  uspgrsprf1  49071  1odd  49094  nnsgrp  49100  0even  49160  2even  49162  2zrngamgm  49168  2zrngasgrp  49169  2zrngamnd  49170  2zrngagrp  49172  2zrngmsgrp  49176  zlmodzxzldeplem3  49440  lvecpsslmod  49445  ldepsnlinc  49446  blennngt2o2  49530  blennn0e2  49532  ackval42  49634  rrx2xpref1o  49656  rrx2plordisom  49661  slotresfo  49833  sepfsepc  49862  basresposfo  49912  oppff1  50082  setcsnterm  50424  setc1onsubc  50536  setrec2lem2  50628  aacllem  50780  veroquadmodzerod  50825  veroquadnolindfd  50826