Theorem mpbir2an 717

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

Syntax hints:   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  3pm3.2i  1346  euequ  2601  eqssi  3938  elini  4135  dtruALT2  5306  exexneq  5381  opnzi  5421  so0  5571  we0  5620  difxp  6122  ord0  6371  dfiota4  6484  funi  6524  funcnvsn  6542  idfn  6620  fn0  6623  f0  6715  fconst  6720  f10  6807  f1o0  6811  f1oiOLD  6813  f1osn  6815  isoid  7280  porpss  7677  epweon  7725  epweonALT  7726  ordon  7727  omssnlim  7828  peano1  7836  fo1st  7958  fo2nd  7959  soseq  8106  iordsmo  8294  tfrlem7  8319  tfr1  8333  frfnom  8371  seqomlem2  8387  oawordeulem  8486  1onn  8573  2onn  8575  naddf  8614  mapsnf1o2  8839  canth2  9065  1sdom2  9155  unfilem2  9213  cantnfvalf  9584  cnfcom3clem  9624  ssttrcl  9634  tc2  9659  r111  9697  rankf  9716  cardf2  9865  harcard  9900  r0weon  9932  infxpenc  9938  infxpenc2lem1  9939  alephon  9989  alephf1  10005  alephiso  10018  alephsmo  10022  alephf1ALT  10023  alephfplem4  10027  ackbij1lem17  10155  ackbij1  10157  ackbij2  10162  fin1a2lem2  10321  fin1a2lem4  10323  axcc2lem  10356  iunfo  10459  smobeth  10507  0tsk  10676  1pi  10804  nqerf  10851  axaddf  11066  axmulf  11067  axicn  11071  mpoaddf  11130  mpomulf  11131  mulnzcnf  11794  negiso  12134  dfnn2  12185  nnind  12190  0z  12533  dfuzi  12618  cnref1o  12933  elrpii  12943  0e0icopnf  13409  0e0iccpnf  13410  fldiv4p1lem1div2  13792  om2uzf1oi  13913  om2uzisoi  13914  uzrdgfni  13918  expcl2lem  14033  expclzlem  14043  expge0  14058  expge1  14059  faclbnd4lem1  14253  hashkf  14292  wwlktovf1  14917  sqrtf  15324  fclim  15513  fprodn0f  15954  eff2  16064  reeff1  16085  ef01bndlem  16149  sin01bnd  16150  cos01bnd  16151  sin01gt0  16155  egt2lt3  16171  qnnen  16178  ruc  16208  halfleoddlt  16329  divalglem2  16362  divalglem9  16368  bitsf1  16413  sadaddlem  16433  2prm  16659  3prm  16661  1arith  16896  prmlem1a  17075  setsnid  17176  xpsff1o  17529  dmaf  18014  cdaf  18015  coapm  18036  0pos  18285  isposi  18287  letsr  18557  ex-chn1  18601  ex-chn2  18602  sgrp0b  18694  frmdplusg  18820  efmndsgrp  18852  smndex1sgrp  18877  smndex1mnd  18879  symg2bas  19366  pmtrsn  19492  odf  19510  efgsfo  19712  efgrelexlemb  19723  isabli  19769  rngmgpf  20136  mgpf  20227  prdscrngd  20299  xrsmgmdifsgrp  21391  cnmgpid  21411  xrs1cmn  21424  xrge0omnd  21427  zringnzr  21442  zringunit  21448  zringlpir  21449  zringndrg  21450  pzriprnglem5  21467  pzriprnglem7  21469  pzriprnglem9  21471  pzriprnglem13  21475  zzngim  21534  cnmsgngrp  21561  psgninv  21564  zrhpsgnmhm  21566  retos  21600  refld  21601  rzgrp  21605  pjpm  21690  fntopon  22914  istpsi  22932  cmpfi  23398  indisconn  23408  kqf  23737  fbssfi  23827  zfbas  23886  ptcmplem2  24043  prdstmdd  24114  tsmsfbas  24118  ismeti  24315  prdsxmslem2  24519  cnfldms  24765  cnnrg  24770  tgqioo  24790  xrtgioo  24797  recld2  24805  xrge0gsumle  24824  xrge0tsms  24825  addcnlem  24855  divcn  24860  abscncf  24893  recncf  24894  imcncf  24895  cjcncf  24896  icopnfhmeo  24935  xrhmeo  24938  cnllycmp  24948  isclmi0  25090  iscvsi  25121  cnstrcvs  25133  cncms  25347  ovolf  25474  ovolre  25517  opnmblALT  25595  dveflem  25971  mdegxrf  26058  iaa  26316  ulmdm  26383  dvradcnv  26411  reeff1o  26437  reefiso  26438  reefgim  26440  recosf1o  26524  efifo  26536  logcn  26636  cxpcn3  26737  resqrtcn  26738  logb1  26758  logbmpt  26777  2logb9irrALT  26787  sqrt2cxp2logb9e3  26788  ressatans  26923  lgamcvg2  27043  lgam1  27052  gam1  27053  efnnfsumcl  27091  efchtdvds  27147  ppiub  27192  lgslem2  27286  lgsfcl2  27291  lgsne0  27323  2lgslem1b  27380  padicabvf  27619  bdayfo  27666  cutsf  27809  madef  27853  cutsfo  27922  addsf  27999  addsfo  28000  negsf  28069  negsfo  28070  negsf1o  28071  subsfo  28082  0ons  28273  1ons  28274  oniso  28288  dfn0s2  28349  1nns  28366  bdayn0sf1o  28387  zsoring  28426  twocut  28440  0reno  28513  1reno  28514  istrkg3ld  28554  axlowdimlem16  29051  upgrbi  29187  umgrbi  29195  lfuhgr1v0e  29348  cusgr0  29520  wlk2v2elem2  30251  upgr4cycl4dv4e  30280  konigsberglem4  30350  frgr0  30360  ex-pss  30523  ex-fl  30542  ex-mod  30544  isgrpoi  30594  grporn  30617  isabloi  30647  smcnlem  30793  lnocoi  30853  cncph  30915  cnbn  30965  cnchl  31012  norm3adifii  31244  hhph  31274  hhhl  31300  hlim0  31331  hlimf  31333  helch  31339  hsn0elch  31344  hhssabloilem  31357  hhssnv  31360  hhshsslem2  31364  hhssbnOLD  31375  shscli  31413  shintcli  31425  chintcli  31427  shsval2i  31483  pjhthlem2  31488  lejdii  31634  nonbooli  31747  pjrni  31798  pjfoi  31799  pjfi  31800  pjmf1  31812  df0op2  31848  idunop  32074  0cnop  32075  0cnfn  32076  idcnop  32077  idhmop  32078  0hmop  32079  0lnfn  32081  0bdop  32089  lnophsi  32097  lnopcoi  32099  lnopunii  32108  lnophmi  32114  nmcopex  32125  nmcoplb  32126  nmcfnex  32149  nmcfnlb  32150  imaelshi  32154  nlelshi  32156  nlelchi  32157  riesz4i  32159  riesz4  32160  riesz1  32161  cnlnadjlem6  32168  cnlnadjlem9  32171  cnlnadjeui  32173  cnlnadjeu  32174  nmopadji  32186  bdophsi  32192  bdopcoi  32194  nmopcoadji  32197  pjhmopi  32242  pjbdlni  32245  hmopidmchi  32247  mdslj1i  32415  rinvf1o  32729  nnindf  32919  rpdp2cl  32967  dp2ltc  32972  dpmul4  32999  s3clhash  33034  xrstos  33096  xrsclat  33097  xrge0tsmsd  33161  qfld  33388  cnfldfld  33432  reofld  33433  nn0archi  33437  zringidom  33641  zringfrac  33644  ccfldextrr  33837  ccfldsrarelvec  33862  ccfldextdgrr  33863  2sqr3minply  33971  xrge0iifmhm  34130  xrge0pluscn  34131  cnzh  34159  rezh  34160  qqhval2lem  34172  esum0  34240  esumcst  34254  esumpcvgval  34269  esumcvg  34277  dmvlsiga  34320  measdivcstALTV  34416  eulerpartlemt  34562  coinfliprv  34674  ballotlem2  34680  signswmnd  34748  logdivsqrle  34841  hgt750lem  34842  bnj906  35119  xoromon  35277  fineqvnttrclse  35312  indispconn  35469  cnllysconn  35480  rellysconn  35486  msrf  35777  brbigcup  36131  fobigcup  36133  brsingle  36150  fnsingle  36152  brimage  36159  funimage  36161  fnimage  36162  imageval  36163  brcart  36165  brapply  36171  brcup  36172  brcap  36173  funpartfun  36178  brub  36189  mpomulnzcnf  36534  onsucconni  36672  onsucsuccmpi  36678  dnicn  36805  bj-nnfv  37118  bj-wnfnf  37133  bj-nnfa1  37134  bj-nnfe1  37135  bj-rabtr  37290  bj-axreprepsep  37435  taupilem2  37689  taupi  37690  f1omptsnlem  37705  icoreresf  37721  relowlpssretop  37733  finxpreclem3  37762  matunitlindf  37992  mblfinlem2  38032  areacirc  38087  0totbnd  38147  heiborlem6  38190  dfsucmap3  38837  refrelid  38976  idsymrel  39019  trrelressn  39041  refrelsredund4  39090  refrelredund4  39093  disjALTV0  39228  disjALTVid  39229  antisymrelressn  39241  isolatiN  39715  isomliN  39738  ishlatiN  39854  mzpclall  43183  jm2.20nn  43449  dfacbasgrp  43560  dgraaf  43599  onexoegt  43696  omnord1  43757  oege2  43759  oenord1  43768  cantnftermord  43772  cantnf2  43777  omabs2  43784  omcl2  43785  ifpim3  43947  ifpim4  43949  ifpbi1b  43954  eu0  43971  omiscard  43994  iso0  44758  dvsid  44782  rankrelp  45411  halffl  45751  resincncf  46325  0cnf  46327  iblempty  46415  dirkeritg  46552  fourierdlem62  46618  fourierdlem76  46632  fourierdlem103  46659  etransclem18  46702  etransclem46  46730  abnotbtaxb  47385  dfaiota3  47562  ceilhalf1  47808  sprsymrelf1  47978  fmtnof1  48020  fmtno4prm  48060  prmdvdsfmtnof1  48072  31prm  48082  requad01  48119  0evenALTV  48186  1oddALTV  48188  2evenALTV  48190  6even  48209  8even  48211  6gbe  48269  7gbow  48270  8gbe  48271  9gbo  48272  11gbo  48273  usgrexmpl1lem  48519  usgrexmpl2lem  48524  usgrexmpl2trifr  48535  gpg5grlim  48591  gpg5grlic  48592  uspgrsprf1  48645  1odd  48669  nnsgrp  48675  0even  48735  2even  48737  2zrngamgm  48743  2zrngasgrp  48744  2zrngamnd  48745  2zrngagrp  48747  2zrngmsgrp  48751  zlmodzxzldeplem3  49000  lvecpsslmod  49005  ldepsnlinc  49006  blennngt2o2  49090  blennn0e2  49092  ackval42  49194  rrx2xpref1o  49216  rrx2plordisom  49221  slotresfo  49396  sepfsepc  49425  basresposfo  49475  oppff1  49645  setcsnterm  49987  setc1onsubc  50099  setrec2lem2  50191  aacllem  50298