Theorem mpbir2an 712

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 710	. 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  1341  euequ  2598  eqssi  3952  elini  4153  dtruALT2  5317  exexneq  5391  opnzi  5430  so0  5578  we0  5627  difxp  6130  ord0  6379  dfiota4  6492  funi  6532  funcnvsn  6550  idfn  6628  fn0  6631  f0  6723  fconst  6728  f10  6815  f1o0  6819  f1oiOLD  6821  f1osn  6823  isoid  7285  porpss  7682  epweon  7730  epweonALT  7731  ordon  7732  omssnlim  7833  peano1  7841  fo1st  7963  fo2nd  7964  soseq  8111  iordsmo  8299  tfrlem7  8324  tfr1  8338  frfnom  8376  seqomlem2  8392  oawordeulem  8491  1onn  8578  2onn  8580  naddf  8619  mapsnf1o2  8844  canth2  9070  1sdom2  9160  unfilem2  9218  cantnfvalf  9586  cnfcom3clem  9626  ssttrcl  9636  tc2  9661  r111  9699  rankf  9718  cardf2  9867  harcard  9902  r0weon  9934  infxpenc  9940  infxpenc2lem1  9941  alephon  9991  alephf1  10007  alephiso  10020  alephsmo  10024  alephf1ALT  10025  alephfplem4  10029  ackbij1lem17  10157  ackbij1  10159  ackbij2  10164  fin1a2lem2  10323  fin1a2lem4  10325  axcc2lem  10358  iunfo  10461  smobeth  10509  0tsk  10678  1pi  10806  nqerf  10853  axaddf  11068  axmulf  11069  axicn  11073  mpoaddf  11132  mpomulf  11133  mulnzcnf  11795  negiso  12134  dfnn2  12170  nnind  12175  0z  12511  dfuzi  12595  cnref1o  12910  elrpii  12920  0e0icopnf  13386  0e0iccpnf  13387  fldiv4p1lem1div2  13767  om2uzf1oi  13888  om2uzisoi  13889  uzrdgfni  13893  expcl2lem  14008  expclzlem  14018  expge0  14033  expge1  14034  faclbnd4lem1  14228  hashkf  14267  wwlktovf1  14892  sqrtf  15299  fclim  15488  fprodn0f  15926  eff2  16036  reeff1  16057  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  sin01gt0  16127  egt2lt3  16143  qnnen  16150  ruc  16180  halfleoddlt  16301  divalglem2  16334  divalglem9  16340  bitsf1  16385  sadaddlem  16405  2prm  16631  3prm  16633  1arith  16867  prmlem1a  17046  setsnid  17147  xpsff1o  17500  dmaf  17985  cdaf  17986  coapm  18007  0pos  18256  isposi  18258  letsr  18528  ex-chn1  18572  ex-chn2  18573  sgrp0b  18665  frmdplusg  18791  efmndsgrp  18823  smndex1sgrp  18845  smndex1mnd  18847  symg2bas  19334  pmtrsn  19460  odf  19478  efgsfo  19680  efgrelexlemb  19691  isabli  19737  rngmgpf  20104  mgpf  20195  prdscrngd  20269  xrsmgmdifsgrp  21375  cnmgpid  21396  xrs1cmn  21409  xrge0omnd  21412  zringnzr  21427  zringunit  21433  zringlpir  21434  zringndrg  21435  pzriprnglem5  21452  pzriprnglem7  21454  pzriprnglem9  21456  pzriprnglem13  21460  zzngim  21519  cnmsgngrp  21546  psgninv  21549  zrhpsgnmhm  21551  retos  21585  refld  21586  rzgrp  21590  pjpm  21675  fntopon  22880  istpsi  22898  cmpfi  23364  indisconn  23374  kqf  23703  fbssfi  23793  zfbas  23852  ptcmplem2  24009  prdstmdd  24080  tsmsfbas  24084  ismeti  24281  prdsxmslem2  24485  cnfldms  24731  cnnrg  24736  tgqioo  24756  xrtgioo  24763  recld2  24771  xrge0gsumle  24790  xrge0tsms  24791  addcnlem  24821  divcnOLD  24825  divcn  24827  abscncf  24862  recncf  24863  imcncf  24864  cjcncf  24865  icopnfhmeo  24909  xrhmeo  24912  cnllycmp  24923  isclmi0  25066  iscvsi  25097  cnstrcvs  25109  cncms  25323  ovolf  25451  ovolre  25494  opnmblALT  25572  dveflem  25951  mdegxrf  26041  iaa  26301  ulmdm  26370  dvradcnv  26398  reeff1o  26425  reefiso  26426  reefgim  26428  recosf1o  26512  efifo  26524  logcn  26624  cxpcn3  26726  resqrtcn  26727  logb1  26747  logbmpt  26766  2logb9irrALT  26776  sqrt2cxp2logb9e3  26777  ressatans  26912  lgamcvg2  27033  lgam1  27042  gam1  27043  efnnfsumcl  27081  efchtdvds  27137  ppiub  27183  lgslem2  27277  lgsfcl2  27282  lgsne0  27314  2lgslem1b  27371  padicabvf  27610  bdayfo  27657  cutsf  27800  madef  27844  cutsfo  27913  addsf  27990  addsfo  27991  negsf  28060  negsfo  28061  negsf1o  28062  subsfo  28073  0ons  28264  1ons  28265  oniso  28279  dfn0s2  28340  1nns  28357  bdayn0sf1o  28378  zsoring  28417  twocut  28431  0reno  28504  1reno  28505  istrkg3ld  28545  axlowdimlem16  29042  upgrbi  29178  umgrbi  29186  lfuhgr1v0e  29339  cusgr0  29511  wlk2v2elem2  30243  upgr4cycl4dv4e  30272  konigsberglem4  30342  frgr0  30352  ex-pss  30515  ex-fl  30534  ex-mod  30536  isgrpoi  30585  grporn  30608  isabloi  30638  smcnlem  30784  lnocoi  30844  cncph  30906  cnbn  30956  cnchl  31003  norm3adifii  31235  hhph  31265  hhhl  31291  hlim0  31322  hlimf  31324  helch  31330  hsn0elch  31335  hhssabloilem  31348  hhssnv  31351  hhshsslem2  31355  hhssbnOLD  31366  shscli  31404  shintcli  31416  chintcli  31418  shsval2i  31474  pjhthlem2  31479  lejdii  31625  nonbooli  31738  pjrni  31789  pjfoi  31790  pjfi  31791  pjmf1  31803  df0op2  31839  idunop  32065  0cnop  32066  0cnfn  32067  idcnop  32068  idhmop  32069  0hmop  32070  0lnfn  32072  0bdop  32080  lnophsi  32088  lnopcoi  32090  lnopunii  32099  lnophmi  32105  nmcopex  32116  nmcoplb  32117  nmcfnex  32140  nmcfnlb  32141  imaelshi  32145  nlelshi  32147  nlelchi  32148  riesz4i  32150  riesz4  32151  riesz1  32152  cnlnadjlem6  32159  cnlnadjlem9  32162  cnlnadjeui  32164  cnlnadjeu  32165  nmopadji  32177  bdophsi  32183  bdopcoi  32185  nmopcoadji  32188  pjhmopi  32233  pjbdlni  32236  hmopidmchi  32238  mdslj1i  32406  rinvf1o  32719  nnindf  32910  rpdp2cl  32973  dp2ltc  32978  dpmul4  33005  s3clhash  33040  xrstos  33102  xrsclat  33103  xrge0tsmsd  33166  qfld  33390  cnfldfld  33434  reofld  33435  nn0archi  33439  zringidom  33643  zringfrac  33646  ccfldextrr  33823  ccfldsrarelvec  33848  ccfldextdgrr  33849  2sqr3minply  33957  xrge0iifmhm  34116  xrge0pluscn  34117  cnzh  34145  rezh  34146  qqhval2lem  34158  esum0  34226  esumcst  34240  esumpcvgval  34255  esumcvg  34263  dmvlsiga  34306  measdivcstALTV  34402  eulerpartlemt  34548  coinfliprv  34660  ballotlem2  34666  signswmnd  34734  logdivsqrle  34827  hgt750lem  34828  bnj906  35105  xoromon  35264  fineqvnttrclse  35299  indispconn  35447  cnllysconn  35458  rellysconn  35464  msrf  35755  brbigcup  36109  fobigcup  36111  brsingle  36128  fnsingle  36130  brimage  36137  funimage  36139  fnimage  36140  imageval  36141  brcart  36143  brapply  36149  brcup  36150  brcap  36151  funpartfun  36156  brub  36167  mpomulnzcnf  36512  onsucconni  36650  onsucsuccmpi  36656  dnicn  36711  bj-nnfv  37005  bj-wnfnf  37015  bj-nnfa1  37016  bj-nnfe1  37017  bj-rabtr  37172  bj-axreprepsep  37317  taupilem2  37571  taupi  37572  f1omptsnlem  37585  icoreresf  37601  relowlpssretop  37613  finxpreclem3  37642  matunitlindf  37863  mblfinlem2  37903  areacirc  37958  0totbnd  38018  heiborlem6  38061  dfsucmap3  38708  refrelid  38847  idsymrel  38890  trrelressn  38912  refrelsredund4  38961  refrelredund4  38964  disjALTV0  39099  disjALTVid  39100  antisymrelressn  39112  isolatiN  39586  isomliN  39609  ishlatiN  39725  mzpclall  43078  jm2.20nn  43348  dfacbasgrp  43459  dgraaf  43498  onexoegt  43595  omnord1  43656  oege2  43658  oenord1  43667  cantnftermord  43671  cantnf2  43676  omabs2  43683  omcl2  43684  ifpim3  43846  ifpim4  43848  ifpbi1b  43853  eu0  43870  omiscard  43893  iso0  44657  dvsid  44681  rankrelp  45310  halffl  45652  resincncf  46227  0cnf  46229  iblempty  46317  dirkeritg  46454  fourierdlem62  46520  fourierdlem76  46534  fourierdlem103  46561  etransclem18  46604  etransclem46  46632  abnotbtaxb  47269  dfaiota3  47446  ceilhalf1  47688  sprsymrelf1  47850  fmtnof1  47889  fmtno4prm  47929  prmdvdsfmtnof1  47941  31prm  47951  requad01  47975  0evenALTV  48042  1oddALTV  48044  2evenALTV  48046  6even  48065  8even  48067  6gbe  48125  7gbow  48126  8gbe  48127  9gbo  48128  11gbo  48129  usgrexmpl1lem  48375  usgrexmpl2lem  48380  usgrexmpl2trifr  48391  gpg5grlim  48447  gpg5grlic  48448  uspgrsprf1  48501  1odd  48525  nnsgrp  48531  0even  48591  2even  48593  2zrngamgm  48599  2zrngasgrp  48600  2zrngamnd  48601  2zrngagrp  48603  2zrngmsgrp  48607  zlmodzxzldeplem3  48856  lvecpsslmod  48861  ldepsnlinc  48862  blennngt2o2  48946  blennn0e2  48948  ackval42  49050  rrx2xpref1o  49072  rrx2plordisom  49077  slotresfo  49252  sepfsepc  49281  basresposfo  49331  oppff1  49501  setcsnterm  49843  setc1onsubc  49955  setrec2lem2  50047  aacllem  50154