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 394

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 395

This theorem is referenced by:  3pm3.2i  1337  euequ  2589  eqssi  3997  elini  4192  dtruALT2  5367  exexneq  5433  dtruOLD  5440  opnzi  5473  so0  5623  we0  5670  difxp  6162  ord0  6416  dfiota4  6534  funi  6579  funcnvsn  6597  idfn  6677  fn0  6680  f0  6771  fconst  6776  f10  6865  f1o0  6869  f1oi  6870  f1osn  6872  isoid  7328  porpss  7719  epweon  7764  epweonALT  7765  ordon  7766  omssnlim  7872  peano1  7881  fo1st  7997  fo2nd  7998  soseq  8147  wfrfunOLD  8321  wfr1OLD  8329  iordsmo  8359  tfrlem7  8385  tfr1  8399  frfnom  8437  seqomlem2  8453  oawordeulem  8556  1onn  8641  2onn  8643  naddf  8682  mapsnf1o2  8890  canth2  9132  1sdom2  9242  unfilem2  9313  cantnfvalf  9662  cnfcom3clem  9702  ssttrcl  9712  tc2  9739  r111  9772  rankf  9791  cardf2  9940  harcard  9975  r0weon  10009  infxpenc  10015  infxpenc2lem1  10016  alephon  10066  alephf1  10082  alephiso  10095  alephsmo  10099  alephf1ALT  10100  alephfplem4  10104  ackbij1lem17  10233  ackbij1  10235  ackbij2  10240  fin1a2lem2  10398  fin1a2lem4  10400  axcc2lem  10433  iunfo  10536  smobeth  10583  0tsk  10752  1pi  10880  nqerf  10927  axaddf  11142  axmulf  11143  axicn  11147  mpomulf  11206  mulnzcnopr  11864  negiso  12198  dfnn2  12229  nnind  12234  0z  12573  dfuzi  12657  cnref1o  12973  elrpii  12981  0e0icopnf  13439  0e0iccpnf  13440  fz0to4untppr  13608  fldiv4p1lem1div2  13804  om2uzf1oi  13922  om2uzisoi  13923  uzrdgfni  13927  expcl2lem  14043  expclzlem  14053  expge0  14068  expge1  14069  faclbnd4lem1  14257  hashkf  14296  wwlktovf1  14912  sqrtf  15314  fclim  15501  fprodn0f  15939  eff2  16046  reeff1  16067  ef01bndlem  16131  sin01bnd  16132  cos01bnd  16133  sin01gt0  16137  egt2lt3  16153  qnnen  16160  ruc  16190  halfleoddlt  16309  divalglem2  16342  divalglem9  16348  bitsf1  16391  sadaddlem  16411  2prm  16633  3prm  16635  1arith  16864  prmlem1a  17044  setsnid  17146  setsnidOLD  17147  xpsff1o  17517  dmaf  18003  cdaf  18004  coapm  18025  0pos  18278  0posOLD  18279  isposi  18281  letsr  18550  sgrp0b  18653  frmdplusg  18771  efmndsgrp  18803  smndex1sgrp  18825  smndex1mnd  18827  symg2bas  19301  pmtrsn  19428  odf  19446  efgsfo  19648  efgrelexlemb  19659  isabli  19705  rngmgpf  20051  mgpf  20142  prdscrngd  20210  xrsmgmdifsgrp  21182  xrs1cmn  21185  cnmgpid  21207  zringnzr  21231  zringunit  21237  zringlpir  21238  zringndrg  21239  pzriprnglem5  21254  pzriprnglem7  21256  pzriprnglem9  21258  pzriprnglem13  21262  zzngim  21327  cnmsgngrp  21351  psgninv  21354  zrhpsgnmhm  21356  retos  21390  refld  21391  rzgrp  21395  pjpm  21482  fntopon  22646  istpsi  22664  cmpfi  23132  indisconn  23142  kqf  23471  fbssfi  23561  zfbas  23620  ptcmplem2  23777  prdstmdd  23848  tsmsfbas  23852  ismeti  24051  prdsxmslem2  24258  cnfldms  24512  cnnrg  24517  tgqioo  24536  xrtgioo  24542  recld2  24550  xrge0gsumle  24569  xrge0tsms  24570  addcnlem  24600  divcnOLD  24604  divcn  24606  abscncf  24641  recncf  24642  imcncf  24643  cjcncf  24644  icopnfhmeo  24688  xrhmeo  24691  cnllycmp  24702  isclmi0  24845  iscvsi  24876  cnstrcvs  24888  cncms  25103  ovolf  25231  ovolre  25274  opnmblALT  25352  dveflem  25731  mdegxrf  25821  iaa  26074  ulmdm  26141  dvradcnv  26169  reeff1o  26195  reefiso  26196  reefgim  26198  recosf1o  26280  efifo  26292  logcn  26391  cxpcn3  26492  resqrtcn  26493  logb1  26510  logbmpt  26529  2logb9irrALT  26539  sqrt2cxp2logb9e3  26540  ressatans  26675  lgamcvg2  26795  lgam1  26804  gam1  26805  efnnfsumcl  26843  efchtdvds  26899  ppiub  26943  lgslem2  27037  lgsfcl2  27042  lgsne0  27074  2lgslem1b  27131  padicabvf  27370  bdayfo  27416  scutf  27550  madef  27588  scutfo  27635  addsf  27704  addsfo  27705  negsf  27765  negsfo  27766  negsf1o  27767  0ons  27922  1ons  27923  dfn0s2  27941  n0sind  27942  istrkg3ld  27979  axlowdimlem16  28482  upgrbi  28620  umgrbi  28628  lfuhgr1v0e  28778  cusgr0  28950  wlk2v2elem2  29676  upgr4cycl4dv4e  29705  konigsberglem4  29775  frgr0  29785  ex-pss  29948  ex-fl  29967  ex-mod  29969  isgrpoi  30018  grporn  30041  isabloi  30071  smcnlem  30217  lnocoi  30277  cncph  30339  cnbn  30389  cnchl  30436  norm3adifii  30668  hhph  30698  hhhl  30724  hlim0  30755  hlimf  30757  helch  30763  hsn0elch  30768  hhssabloilem  30781  hhssnv  30784  hhshsslem2  30788  hhssbnOLD  30799  shscli  30837  shintcli  30849  chintcli  30851  shsval2i  30907  pjhthlem2  30912  lejdii  31058  nonbooli  31171  pjrni  31222  pjfoi  31223  pjfi  31224  pjmf1  31236  df0op2  31272  idunop  31498  0cnop  31499  0cnfn  31500  idcnop  31501  idhmop  31502  0hmop  31503  0lnfn  31505  0bdop  31513  lnophsi  31521  lnopcoi  31523  lnopunii  31532  lnophmi  31538  nmcopex  31549  nmcoplb  31550  nmcfnex  31573  nmcfnlb  31574  imaelshi  31578  nlelshi  31580  nlelchi  31581  riesz4i  31583  riesz4  31584  riesz1  31585  cnlnadjlem6  31592  cnlnadjlem9  31595  cnlnadjeui  31597  cnlnadjeu  31598  nmopadji  31610  bdophsi  31616  bdopcoi  31618  nmopcoadji  31621  pjhmopi  31666  pjbdlni  31669  hmopidmchi  31671  mdslj1i  31839  rinvf1o  32121  nnindf  32292  rpdp2cl  32315  dp2ltc  32320  dpmul4  32347  s3clhash  32381  xrstos  32447  xrsclat  32448  xrge0tsmsd  32479  xrge0omnd  32499  reofld  32729  nn0archi  32732  ccfldextrr  33015  ccfldsrarelvec  33034  ccfldextdgrr  33035  xrge0iifmhm  33217  xrge0pluscn  33218  cnzh  33248  rezh  33249  qqhval2lem  33259  esum0  33345  esumcst  33359  esumpcvgval  33374  esumcvg  33382  dmvlsiga  33425  measdivcstALTV  33521  eulerpartlemt  33668  coinfliprv  33779  ballotlem2  33785  signswmnd  33866  logdivsqrle  33960  hgt750lem  33961  bnj906  34239  indispconn  34523  cnllysconn  34534  rellysconn  34540  msrf  34831  brbigcup  35174  fobigcup  35176  brsingle  35193  fnsingle  35195  brimage  35202  funimage  35204  fnimage  35205  imageval  35206  brcart  35208  brapply  35214  brcup  35215  brcap  35216  funpartfun  35219  brub  35230  mpoaddf  35471  onsucconni  35625  onsucsuccmpi  35631  dnicn  35671  bj-wnfnf  35920  bj-nnfv  35935  bj-nnfa1  35940  bj-nnfe1  35941  bj-rabtr  36113  taupilem2  36506  taupi  36507  f1omptsnlem  36520  icoreresf  36536  relowlpssretop  36548  finxpreclem3  36577  matunitlindf  36789  mblfinlem2  36829  areacirc  36884  0totbnd  36944  heiborlem6  36987  refrelid  37695  idsymrel  37734  trrelressn  37756  refrelsredund4  37805  refrelredund4  37808  disjALTV0  37927  disjALTVid  37928  antisymrelressn  37937  isolatiN  38389  isomliN  38412  ishlatiN  38528  mzpclall  41767  jm2.20nn  42038  dfacbasgrp  42152  dgraaf  42191  onexoegt  42295  omnord1  42357  oege2  42359  oenord1  42368  cantnftermord  42372  cantnf2  42377  omabs2  42384  omcl2  42385  ifpim3  42549  ifpim4  42551  ifpbi1b  42556  eu0  42573  omiscard  42596  iso0  43368  dvsid  43392  halffl  44304  resincncf  44889  0cnf  44891  iblempty  44979  dirkeritg  45116  fourierdlem62  45182  fourierdlem76  45196  fourierdlem103  45223  etransclem18  45266  etransclem46  45294  abnotbtaxb  45923  dfaiota3  46098  sprsymrelf1  46462  fmtnof1  46501  fmtno4prm  46541  prmdvdsfmtnof1  46553  31prm  46563  requad01  46587  0evenALTV  46654  1oddALTV  46656  2evenALTV  46658  6even  46677  8even  46679  6gbe  46737  7gbow  46738  8gbe  46739  9gbo  46740  11gbo  46741  uspgrsprf1  46823  1odd  46847  nnsgrp  46853  0even  46917  2even  46919  2zrngamgm  46925  2zrngasgrp  46926  2zrngamnd  46927  2zrngagrp  46929  2zrngmsgrp  46933  zlmodzxzldeplem3  47270  lvecpsslmod  47275  ldepsnlinc  47276  blennngt2o2  47365  blennn0e2  47367  ackval42  47469  rrx2xpref1o  47491  rrx2plordisom  47496  sepfsepc  47647  setrec2lem2  47826  aacllem  47935