Theorem mpbir2an 707

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

Syntax hints:   ↔ wb 205   ∧ wa 395

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 396

This theorem is referenced by:  3pm3.2i  1337  euequ  2597  eqssi  3933  elini  4123  dtru  5288  opnzi  5383  so0  5530  we0  5575  difxp  6056  ord0  6303  dfiota4  6410  funi  6450  funcnvsn  6468  idfn  6544  fnresiOLD  6546  fn0  6548  f0  6639  fconst  6644  f10  6732  f1o0  6736  f1oi  6737  f1osn  6739  isoid  7180  porpss  7558  epweon  7603  ordon  7604  omssnlim  7702  fo1st  7824  fo2nd  7825  wfrfunOLD  8121  wfr1OLD  8129  iordsmo  8159  tfrlem7  8185  tfr1  8199  frfnom  8236  seqomlem2  8252  oawordeulem  8347  mapsnf1o2  8640  canth2  8866  unfilem2  9009  cantnfvalf  9353  cnfcom3clem  9393  tc2  9431  r111  9464  rankf  9483  cardf2  9632  harcard  9667  r0weon  9699  infxpenc  9705  infxpenc2lem1  9706  alephon  9756  alephf1  9772  alephiso  9785  alephsmo  9789  alephf1ALT  9790  alephfplem4  9794  ackbij1lem17  9923  ackbij1  9925  ackbij2  9930  fin1a2lem2  10088  fin1a2lem4  10090  axcc2lem  10123  iunfo  10226  smobeth  10273  0tsk  10442  1pi  10570  nqerf  10617  axaddf  10832  axmulf  10833  axicn  10837  mulnzcnopr  11551  negiso  11885  dfnn2  11916  nnind  11921  0z  12260  dfuzi  12341  cnref1o  12654  elrpii  12662  0e0icopnf  13119  0e0iccpnf  13120  fz0to4untppr  13288  fldiv4p1lem1div2  13483  om2uzf1oi  13601  om2uzisoi  13602  uzrdgfni  13606  expcl2lem  13722  expclzlem  13734  expge0  13747  expge1  13748  faclbnd4lem1  13935  hashkf  13974  wwlktovf1  14600  sqrtf  15003  fclim  15190  fprodn0f  15629  eff2  15736  reeff1  15757  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  egt2lt3  15843  qnnen  15850  ruc  15880  halfleoddlt  15999  divalglem2  16032  divalglem9  16038  bitsf1  16081  sadaddlem  16101  2prm  16325  3prm  16327  1arith  16556  prmlem1a  16736  setsnid  16838  setsnidOLD  16839  xpsff1o  17195  dmaf  17680  cdaf  17681  coapm  17702  0pos  17954  0posOLD  17955  isposi  17957  letsr  18226  sgrp0b  18298  frmdplusg  18408  efmndsgrp  18440  smndex1sgrp  18462  smndex1mnd  18464  symg2bas  18915  pmtrsn  19042  odf  19060  efgsfo  19260  efgrelexlemb  19271  isabli  19316  mgpf  19713  prdscrngd  19767  xrsmgmdifsgrp  20547  xrs1cmn  20550  cnmgpid  20572  zringnzr  20594  zringunit  20600  zringlpir  20601  zringndrg  20602  zzngim  20672  cnmsgngrp  20696  psgninv  20699  zrhpsgnmhm  20701  retos  20735  refld  20736  rzgrp  20740  pjpm  20825  fntopon  21981  istpsi  21999  cmpfi  22467  indisconn  22477  kqf  22806  fbssfi  22896  zfbas  22955  ptcmplem2  23112  prdstmdd  23183  tsmsfbas  23187  ismeti  23386  prdsxmslem2  23591  cnfldms  23845  cnnrg  23850  tgqioo  23869  xrtgioo  23875  recld2  23883  xrge0gsumle  23902  xrge0tsms  23903  addcnlem  23933  divcn  23937  abscncf  23970  recncf  23971  imcncf  23972  cjcncf  23973  icopnfhmeo  24012  xrhmeo  24015  cnllycmp  24025  isclmi0  24167  iscvsi  24198  cnstrcvs  24210  cncms  24424  ovolf  24551  ovolre  24594  opnmblALT  24672  dveflem  25048  mdegxrf  25138  iaa  25390  ulmdm  25457  dvradcnv  25485  reeff1o  25511  reefiso  25512  reefgim  25514  recosf1o  25596  efifo  25608  logcn  25707  cxpcn3  25806  resqrtcn  25807  logb1  25824  logbmpt  25843  2logb9irrALT  25853  sqrt2cxp2logb9e3  25854  ressatans  25989  lgamcvg2  26109  lgam1  26118  gam1  26119  efnnfsumcl  26157  efchtdvds  26213  ppiub  26257  lgslem2  26351  lgsfcl2  26356  lgsne0  26388  2lgslem1b  26445  padicabvf  26684  istrkg3ld  26726  axlowdimlem16  27228  upgrbi  27366  umgrbi  27374  lfuhgr1v0e  27524  cusgr0  27696  wlk2v2elem2  28421  upgr4cycl4dv4e  28450  konigsberglem4  28520  frgr0  28530  ex-pss  28693  ex-fl  28712  ex-mod  28714  isgrpoi  28761  grporn  28784  isabloi  28814  smcnlem  28960  lnocoi  29020  cncph  29082  cnbn  29132  cnchl  29179  norm3adifii  29411  hhph  29441  hhhl  29467  hlim0  29498  hlimf  29500  helch  29506  hsn0elch  29511  hhssabloilem  29524  hhssnv  29527  hhshsslem2  29531  hhssbnOLD  29542  shscli  29580  shintcli  29592  chintcli  29594  shsval2i  29650  pjhthlem2  29655  lejdii  29801  nonbooli  29914  pjrni  29965  pjfoi  29966  pjfi  29967  pjmf1  29979  df0op2  30015  idunop  30241  0cnop  30242  0cnfn  30243  idcnop  30244  idhmop  30245  0hmop  30246  0lnfn  30248  0bdop  30256  lnophsi  30264  lnopcoi  30266  lnopunii  30275  lnophmi  30281  nmcopex  30292  nmcoplb  30293  nmcfnex  30316  nmcfnlb  30317  imaelshi  30321  nlelshi  30323  nlelchi  30324  riesz4i  30326  riesz4  30327  riesz1  30328  cnlnadjlem6  30335  cnlnadjlem9  30338  cnlnadjeui  30340  cnlnadjeu  30341  nmopadji  30353  bdophsi  30359  bdopcoi  30361  nmopcoadji  30364  pjhmopi  30409  pjbdlni  30412  hmopidmchi  30414  mdslj1i  30582  rinvf1o  30866  nnindf  31035  rpdp2cl  31058  dp2ltc  31063  dpmul4  31090  s3clhash  31124  xrstos  31190  xrsclat  31191  xrge0tsmsd  31219  xrge0omnd  31239  reofld  31446  nn0archi  31449  ccfldextrr  31625  ccfldsrarelvec  31643  ccfldextdgrr  31644  xrge0iifmhm  31791  xrge0pluscn  31792  cnzh  31820  rezh  31821  qqhval2lem  31831  esum0  31917  esumcst  31931  esumpcvgval  31946  esumcvg  31954  dmvlsiga  31997  measdivcstALTV  32093  eulerpartlemt  32238  coinfliprv  32349  ballotlem2  32355  signswmnd  32436  logdivsqrle  32530  hgt750lem  32531  bnj906  32810  indispconn  33096  cnllysconn  33107  rellysconn  33113  msrf  33404  ssttrcl  33701  soseq  33730  bdayfo  33807  scutf  33933  madef  33967  scutfo  34011  brbigcup  34127  fobigcup  34129  brsingle  34146  fnsingle  34148  brimage  34155  funimage  34157  fnimage  34158  imageval  34159  brcart  34161  brapply  34167  brcup  34168  brcap  34169  funpartfun  34172  brub  34183  onsucconni  34553  onsucsuccmpi  34559  dnicn  34599  bj-wnfnf  34848  bj-nnfv  34863  bj-nnfa1  34868  bj-nnfe1  34869  bj-dtru  34926  bj-rabtr  35045  taupilem2  35420  taupi  35421  f1omptsnlem  35434  icoreresf  35450  relowlpssretop  35462  finxpreclem3  35491  matunitlindf  35702  mblfinlem2  35742  areacirc  35797  0totbnd  35858  heiborlem6  35901  refrelid  36566  idsymrel  36602  refrelsredund4  36672  refrelredund4  36675  disjALTV0  36789  disjALTVid  36790  isolatiN  37157  isomliN  37180  ishlatiN  37296  sn-dtru  40116  mzpclall  40465  jm2.20nn  40735  dfacbasgrp  40849  dgraaf  40888  ifpim3  41001  ifpim4  41003  ifpbi1b  41008  eu0  41025  iso0  41814  dvsid  41838  halffl  42725  resincncf  43306  0cnf  43308  iblempty  43396  dirkeritg  43533  fourierdlem62  43599  fourierdlem76  43613  fourierdlem103  43640  etransclem18  43683  etransclem46  43711  abnotbtaxb  44297  dfaiota3  44471  sprsymrelf1  44836  fmtnof1  44875  fmtno4prm  44915  prmdvdsfmtnof1  44927  31prm  44937  requad01  44961  0evenALTV  45028  1oddALTV  45030  2evenALTV  45032  6even  45051  8even  45053  6gbe  45111  7gbow  45112  8gbe  45113  9gbo  45114  11gbo  45115  uspgrsprf1  45197  1odd  45253  nnsgrp  45259  0even  45377  2even  45379  2zrngamgm  45385  2zrngasgrp  45386  2zrngamnd  45387  2zrngagrp  45389  2zrngmsgrp  45393  zlmodzxzldeplem3  45731  lvecpsslmod  45736  ldepsnlinc  45737  blennngt2o2  45826  blennn0e2  45828  ackval42  45930  rrx2xpref1o  45952  rrx2plordisom  45957  sepfsepc  46109  setrec2lem2  46286  aacllem  46391