Theorem mpbir2an 711

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

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

This theorem is referenced by:  3pm3.2i  1340  euequ  2596  eqssi  3975  elini  4174  dtruALT2  5340  exexneq  5409  dtruOLD  5416  opnzi  5449  so0  5599  we0  5649  difxp  6153  ord0  6406  dfiota4  6522  funi  6567  funcnvsn  6585  idfn  6665  fn0  6668  f0  6758  fconst  6763  f10  6850  f1o0  6854  f1oi  6855  f1osn  6857  isoid  7321  porpss  7719  epweon  7767  epweonALT  7768  ordon  7769  omssnlim  7874  peano1  7882  fo1st  8006  fo2nd  8007  soseq  8156  wfrfunOLD  8331  wfr1OLD  8339  iordsmo  8369  tfrlem7  8395  tfr1  8409  frfnom  8447  seqomlem2  8463  oawordeulem  8564  1onn  8650  2onn  8652  naddf  8691  mapsnf1o2  8906  canth2  9142  1sdom2  9246  unfilem2  9314  cantnfvalf  9677  cnfcom3clem  9717  ssttrcl  9727  tc2  9754  r111  9787  rankf  9806  cardf2  9955  harcard  9990  r0weon  10024  infxpenc  10030  infxpenc2lem1  10031  alephon  10081  alephf1  10097  alephiso  10110  alephsmo  10114  alephf1ALT  10115  alephfplem4  10119  ackbij1lem17  10247  ackbij1  10249  ackbij2  10254  fin1a2lem2  10413  fin1a2lem4  10415  axcc2lem  10448  iunfo  10551  smobeth  10598  0tsk  10767  1pi  10895  nqerf  10942  axaddf  11157  axmulf  11158  axicn  11162  mpoaddf  11221  mpomulf  11222  mulnzcnf  11881  negiso  12220  dfnn2  12251  nnind  12256  0z  12597  dfuzi  12682  cnref1o  12999  elrpii  13009  0e0icopnf  13473  0e0iccpnf  13474  fldiv4p1lem1div2  13850  om2uzf1oi  13969  om2uzisoi  13970  uzrdgfni  13974  expcl2lem  14089  expclzlem  14099  expge0  14114  expge1  14115  faclbnd4lem1  14309  hashkf  14348  wwlktovf1  14974  sqrtf  15380  fclim  15567  fprodn0f  16005  eff2  16115  reeff1  16136  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  sin01gt0  16206  egt2lt3  16222  qnnen  16229  ruc  16259  halfleoddlt  16379  divalglem2  16412  divalglem9  16418  bitsf1  16463  sadaddlem  16483  2prm  16709  3prm  16711  1arith  16945  prmlem1a  17124  setsnid  17225  xpsff1o  17579  dmaf  18060  cdaf  18061  coapm  18082  0pos  18331  isposi  18333  letsr  18601  sgrp0b  18704  frmdplusg  18830  efmndsgrp  18862  smndex1sgrp  18884  smndex1mnd  18886  symg2bas  19372  pmtrsn  19498  odf  19516  efgsfo  19718  efgrelexlemb  19729  isabli  19775  rngmgpf  20115  mgpf  20206  prdscrngd  20280  xrsmgmdifsgrp  21369  xrs1cmn  21372  cnmgpid  21395  zringnzr  21419  zringunit  21425  zringlpir  21426  zringndrg  21427  pzriprnglem5  21444  pzriprnglem7  21446  pzriprnglem9  21448  pzriprnglem13  21452  zzngim  21511  cnmsgngrp  21537  psgninv  21540  zrhpsgnmhm  21542  retos  21576  refld  21577  rzgrp  21581  pjpm  21666  fntopon  22860  istpsi  22878  cmpfi  23344  indisconn  23354  kqf  23683  fbssfi  23773  zfbas  23832  ptcmplem2  23989  prdstmdd  24060  tsmsfbas  24064  ismeti  24262  prdsxmslem2  24466  cnfldms  24712  cnnrg  24717  tgqioo  24737  xrtgioo  24744  recld2  24752  xrge0gsumle  24771  xrge0tsms  24772  addcnlem  24802  divcnOLD  24806  divcn  24808  abscncf  24843  recncf  24844  imcncf  24845  cjcncf  24846  icopnfhmeo  24890  xrhmeo  24893  cnllycmp  24904  isclmi0  25047  iscvsi  25078  cnstrcvs  25090  cncms  25305  ovolf  25433  ovolre  25476  opnmblALT  25554  dveflem  25933  mdegxrf  26023  iaa  26283  ulmdm  26352  dvradcnv  26380  reeff1o  26407  reefiso  26408  reefgim  26410  recosf1o  26494  efifo  26506  logcn  26606  cxpcn3  26708  resqrtcn  26709  logb1  26729  logbmpt  26748  2logb9irrALT  26758  sqrt2cxp2logb9e3  26759  ressatans  26894  lgamcvg2  27015  lgam1  27024  gam1  27025  efnnfsumcl  27063  efchtdvds  27119  ppiub  27165  lgslem2  27259  lgsfcl2  27264  lgsne0  27296  2lgslem1b  27353  padicabvf  27592  bdayfo  27639  scutf  27774  madef  27812  scutfo  27859  addsf  27932  addsfo  27933  negsf  28001  negsfo  28002  negsf1o  28003  subsfo  28012  0ons  28196  1ons  28197  dfn0s2  28253  1nns  28269  nohalf  28324  0reno  28346  istrkg3ld  28386  axlowdimlem16  28882  upgrbi  29018  umgrbi  29026  lfuhgr1v0e  29179  cusgr0  29351  wlk2v2elem2  30083  upgr4cycl4dv4e  30112  konigsberglem4  30182  frgr0  30192  ex-pss  30355  ex-fl  30374  ex-mod  30376  isgrpoi  30425  grporn  30448  isabloi  30478  smcnlem  30624  lnocoi  30684  cncph  30746  cnbn  30796  cnchl  30843  norm3adifii  31075  hhph  31105  hhhl  31131  hlim0  31162  hlimf  31164  helch  31170  hsn0elch  31175  hhssabloilem  31188  hhssnv  31191  hhshsslem2  31195  hhssbnOLD  31206  shscli  31244  shintcli  31256  chintcli  31258  shsval2i  31314  pjhthlem2  31319  lejdii  31465  nonbooli  31578  pjrni  31629  pjfoi  31630  pjfi  31631  pjmf1  31643  df0op2  31679  idunop  31905  0cnop  31906  0cnfn  31907  idcnop  31908  idhmop  31909  0hmop  31910  0lnfn  31912  0bdop  31920  lnophsi  31928  lnopcoi  31930  lnopunii  31939  lnophmi  31945  nmcopex  31956  nmcoplb  31957  nmcfnex  31980  nmcfnlb  31981  imaelshi  31985  nlelshi  31987  nlelchi  31988  riesz4i  31990  riesz4  31991  riesz1  31992  cnlnadjlem6  31999  cnlnadjlem9  32002  cnlnadjeui  32004  cnlnadjeu  32005  nmopadji  32017  bdophsi  32023  bdopcoi  32025  nmopcoadji  32028  pjhmopi  32073  pjbdlni  32076  hmopidmchi  32078  mdslj1i  32246  rinvf1o  32554  nnindf  32744  rpdp2cl  32802  dp2ltc  32807  dpmul4  32834  s3clhash  32869  xrstos  32948  xrsclat  32949  xrge0tsmsd  33002  xrge0omnd  33025  qfld  33237  cnfldfld  33304  reofld  33305  nn0archi  33308  zringidom  33512  zringfrac  33515  ccfldextrr  33634  ccfldsrarelvec  33658  ccfldextdgrr  33659  2sqr3minply  33760  xrge0iifmhm  33916  xrge0pluscn  33917  cnzh  33945  rezh  33946  qqhval2lem  33958  esum0  34026  esumcst  34040  esumpcvgval  34055  esumcvg  34063  dmvlsiga  34106  measdivcstALTV  34202  eulerpartlemt  34349  coinfliprv  34461  ballotlem2  34467  signswmnd  34535  logdivsqrle  34628  hgt750lem  34629  bnj906  34907  indispconn  35202  cnllysconn  35213  rellysconn  35219  msrf  35510  brbigcup  35862  fobigcup  35864  brsingle  35881  fnsingle  35883  brimage  35890  funimage  35892  fnimage  35893  imageval  35894  brcart  35896  brapply  35902  brcup  35903  brcap  35904  funpartfun  35907  brub  35918  mpomulnzcnf  36263  onsucconni  36401  onsucsuccmpi  36407  dnicn  36456  bj-wnfnf  36703  bj-nnfv  36718  bj-nnfa1  36723  bj-nnfe1  36724  bj-rabtr  36894  taupilem2  37286  taupi  37287  f1omptsnlem  37300  icoreresf  37316  relowlpssretop  37328  finxpreclem3  37357  matunitlindf  37588  mblfinlem2  37628  areacirc  37683  0totbnd  37743  heiborlem6  37786  refrelid  38486  idsymrel  38525  trrelressn  38547  refrelsredund4  38596  refrelredund4  38599  disjALTV0  38718  disjALTVid  38719  antisymrelressn  38728  isolatiN  39180  isomliN  39203  ishlatiN  39319  mzpclall  42697  jm2.20nn  42968  dfacbasgrp  43079  dgraaf  43118  onexoegt  43215  omnord1  43276  oege2  43278  oenord1  43287  cantnftermord  43291  cantnf2  43296  omabs2  43303  omcl2  43304  ifpim3  43467  ifpim4  43469  ifpbi1b  43474  eu0  43491  omiscard  43514  iso0  44279  dvsid  44303  rankrelp  44933  halffl  45273  resincncf  45852  0cnf  45854  iblempty  45942  dirkeritg  46079  fourierdlem62  46145  fourierdlem76  46159  fourierdlem103  46186  etransclem18  46229  etransclem46  46257  abnotbtaxb  46892  dfaiota3  47069  ceilhalf1  47311  sprsymrelf1  47458  fmtnof1  47497  fmtno4prm  47537  prmdvdsfmtnof1  47549  31prm  47559  requad01  47583  0evenALTV  47650  1oddALTV  47652  2evenALTV  47654  6even  47673  8even  47675  6gbe  47733  7gbow  47734  8gbe  47735  9gbo  47736  11gbo  47737  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2trifr  47989  gpg5grlic  48041  uspgrsprf1  48070  1odd  48094  nnsgrp  48100  0even  48160  2even  48162  2zrngamgm  48168  2zrngasgrp  48169  2zrngamnd  48170  2zrngagrp  48172  2zrngmsgrp  48176  zlmodzxzldeplem3  48426  lvecpsslmod  48431  ldepsnlinc  48432  blennngt2o2  48520  blennn0e2  48522  ackval42  48624  rrx2xpref1o  48646  rrx2plordisom  48651  slotresfo  48821  sepfsepc  48850  basresposfo  48900  setcsnterm  49323  setc1onsubc  49427  setrec2lem2  49506  aacllem  49613