Theorem mpbir2an 710

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  3pm3.2i  1340  euequ  2592  eqssi  3998  elini  4193  dtruALT2  5368  exexneq  5434  dtruOLD  5441  opnzi  5474  so0  5624  we0  5671  difxp  6161  ord0  6415  dfiota4  6533  funi  6578  funcnvsn  6596  idfn  6676  fn0  6679  f0  6770  fconst  6775  f10  6864  f1o0  6868  f1oi  6869  f1osn  6871  isoid  7323  porpss  7714  epweon  7759  epweonALT  7760  ordon  7761  omssnlim  7867  peano1  7876  fo1st  7992  fo2nd  7993  soseq  8142  wfrfunOLD  8316  wfr1OLD  8324  iordsmo  8354  tfrlem7  8380  tfr1  8394  frfnom  8432  seqomlem2  8448  oawordeulem  8551  1onn  8636  2onn  8638  naddf  8677  mapsnf1o2  8885  canth2  9127  1sdom2  9237  unfilem2  9308  cantnfvalf  9657  cnfcom3clem  9697  ssttrcl  9707  tc2  9734  r111  9767  rankf  9786  cardf2  9935  harcard  9970  r0weon  10004  infxpenc  10010  infxpenc2lem1  10011  alephon  10061  alephf1  10077  alephiso  10090  alephsmo  10094  alephf1ALT  10095  alephfplem4  10099  ackbij1lem17  10228  ackbij1  10230  ackbij2  10235  fin1a2lem2  10393  fin1a2lem4  10395  axcc2lem  10428  iunfo  10531  smobeth  10578  0tsk  10747  1pi  10875  nqerf  10922  axaddf  11137  axmulf  11138  axicn  11142  mulnzcnopr  11857  negiso  12191  dfnn2  12222  nnind  12227  0z  12566  dfuzi  12650  cnref1o  12966  elrpii  12974  0e0icopnf  13432  0e0iccpnf  13433  fz0to4untppr  13601  fldiv4p1lem1div2  13797  om2uzf1oi  13915  om2uzisoi  13916  uzrdgfni  13920  expcl2lem  14036  expclzlem  14046  expge0  14061  expge1  14062  faclbnd4lem1  14250  hashkf  14289  wwlktovf1  14905  sqrtf  15307  fclim  15494  fprodn0f  15932  eff2  16039  reeff1  16060  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  sin01gt0  16130  egt2lt3  16146  qnnen  16153  ruc  16183  halfleoddlt  16302  divalglem2  16335  divalglem9  16341  bitsf1  16384  sadaddlem  16404  2prm  16626  3prm  16628  1arith  16857  prmlem1a  17037  setsnid  17139  setsnidOLD  17140  xpsff1o  17510  dmaf  17996  cdaf  17997  coapm  18018  0pos  18271  0posOLD  18272  isposi  18274  letsr  18543  sgrp0b  18616  frmdplusg  18732  efmndsgrp  18764  smndex1sgrp  18786  smndex1mnd  18788  symg2bas  19255  pmtrsn  19382  odf  19400  efgsfo  19602  efgrelexlemb  19613  isabli  19659  mgpf  20065  prdscrngd  20129  xrsmgmdifsgrp  20975  xrs1cmn  20978  cnmgpid  21000  zringnzr  21022  zringunit  21028  zringlpir  21029  zringndrg  21030  zzngim  21100  cnmsgngrp  21124  psgninv  21127  zrhpsgnmhm  21129  retos  21163  refld  21164  rzgrp  21168  pjpm  21255  fntopon  22418  istpsi  22436  cmpfi  22904  indisconn  22914  kqf  23243  fbssfi  23333  zfbas  23392  ptcmplem2  23549  prdstmdd  23620  tsmsfbas  23624  ismeti  23823  prdsxmslem2  24030  cnfldms  24284  cnnrg  24289  tgqioo  24308  xrtgioo  24314  recld2  24322  xrge0gsumle  24341  xrge0tsms  24342  addcnlem  24372  divcn  24376  abscncf  24409  recncf  24410  imcncf  24411  cjcncf  24412  icopnfhmeo  24451  xrhmeo  24454  cnllycmp  24464  isclmi0  24606  iscvsi  24637  cnstrcvs  24649  cncms  24864  ovolf  24991  ovolre  25034  opnmblALT  25112  dveflem  25488  mdegxrf  25578  iaa  25830  ulmdm  25897  dvradcnv  25925  reeff1o  25951  reefiso  25952  reefgim  25954  recosf1o  26036  efifo  26048  logcn  26147  cxpcn3  26246  resqrtcn  26247  logb1  26264  logbmpt  26283  2logb9irrALT  26293  sqrt2cxp2logb9e3  26294  ressatans  26429  lgamcvg2  26549  lgam1  26558  gam1  26559  efnnfsumcl  26597  efchtdvds  26653  ppiub  26697  lgslem2  26791  lgsfcl2  26796  lgsne0  26828  2lgslem1b  26885  padicabvf  27124  bdayfo  27170  scutf  27303  madef  27341  scutfo  27388  addsf  27456  addsfo  27457  negsf  27516  negsfo  27517  negsf1o  27518  istrkg3ld  27702  axlowdimlem16  28205  upgrbi  28343  umgrbi  28351  lfuhgr1v0e  28501  cusgr0  28673  wlk2v2elem2  29399  upgr4cycl4dv4e  29428  konigsberglem4  29498  frgr0  29508  ex-pss  29671  ex-fl  29690  ex-mod  29692  isgrpoi  29739  grporn  29762  isabloi  29792  smcnlem  29938  lnocoi  29998  cncph  30060  cnbn  30110  cnchl  30157  norm3adifii  30389  hhph  30419  hhhl  30445  hlim0  30476  hlimf  30478  helch  30484  hsn0elch  30489  hhssabloilem  30502  hhssnv  30505  hhshsslem2  30509  hhssbnOLD  30520  shscli  30558  shintcli  30570  chintcli  30572  shsval2i  30628  pjhthlem2  30633  lejdii  30779  nonbooli  30892  pjrni  30943  pjfoi  30944  pjfi  30945  pjmf1  30957  df0op2  30993  idunop  31219  0cnop  31220  0cnfn  31221  idcnop  31222  idhmop  31223  0hmop  31224  0lnfn  31226  0bdop  31234  lnophsi  31242  lnopcoi  31244  lnopunii  31253  lnophmi  31259  nmcopex  31270  nmcoplb  31271  nmcfnex  31294  nmcfnlb  31295  imaelshi  31299  nlelshi  31301  nlelchi  31302  riesz4i  31304  riesz4  31305  riesz1  31306  cnlnadjlem6  31313  cnlnadjlem9  31316  cnlnadjeui  31318  cnlnadjeu  31319  nmopadji  31331  bdophsi  31337  bdopcoi  31339  nmopcoadji  31342  pjhmopi  31387  pjbdlni  31390  hmopidmchi  31392  mdslj1i  31560  rinvf1o  31842  nnindf  32013  rpdp2cl  32036  dp2ltc  32041  dpmul4  32068  s3clhash  32102  xrstos  32168  xrsclat  32169  xrge0tsmsd  32197  xrge0omnd  32217  reofld  32448  nn0archi  32451  ccfldextrr  32716  ccfldsrarelvec  32734  ccfldextdgrr  32735  xrge0iifmhm  32908  xrge0pluscn  32909  cnzh  32939  rezh  32940  qqhval2lem  32950  esum0  33036  esumcst  33050  esumpcvgval  33065  esumcvg  33073  dmvlsiga  33116  measdivcstALTV  33212  eulerpartlemt  33359  coinfliprv  33470  ballotlem2  33476  signswmnd  33557  logdivsqrle  33651  hgt750lem  33652  bnj906  33930  indispconn  34214  cnllysconn  34225  rellysconn  34231  msrf  34522  brbigcup  34859  fobigcup  34861  brsingle  34878  fnsingle  34880  brimage  34887  funimage  34889  fnimage  34890  imageval  34891  brcart  34893  brapply  34899  brcup  34900  brcap  34901  funpartfun  34904  brub  34915  mpomulf  35148  gg-divcn  35152  onsucconni  35311  onsucsuccmpi  35317  dnicn  35357  bj-wnfnf  35606  bj-nnfv  35621  bj-nnfa1  35626  bj-nnfe1  35627  bj-rabtr  35799  taupilem2  36192  taupi  36193  f1omptsnlem  36206  icoreresf  36222  relowlpssretop  36234  finxpreclem3  36263  matunitlindf  36475  mblfinlem2  36515  areacirc  36570  0totbnd  36630  heiborlem6  36673  refrelid  37381  idsymrel  37420  trrelressn  37442  refrelsredund4  37491  refrelredund4  37494  disjALTV0  37613  disjALTVid  37614  antisymrelressn  37623  isolatiN  38075  isomliN  38098  ishlatiN  38214  mzpclall  41451  jm2.20nn  41722  dfacbasgrp  41836  dgraaf  41875  onexoegt  41979  omnord1  42041  oege2  42043  oenord1  42052  cantnftermord  42056  cantnf2  42061  omabs2  42068  omcl2  42069  ifpim3  42233  ifpim4  42235  ifpbi1b  42240  eu0  42257  omiscard  42280  iso0  43052  dvsid  43076  halffl  43993  resincncf  44578  0cnf  44580  iblempty  44668  dirkeritg  44805  fourierdlem62  44871  fourierdlem76  44885  fourierdlem103  44912  etransclem18  44955  etransclem46  44983  abnotbtaxb  45612  dfaiota3  45787  sprsymrelf1  46151  fmtnof1  46190  fmtno4prm  46230  prmdvdsfmtnof1  46242  31prm  46252  requad01  46276  0evenALTV  46343  1oddALTV  46345  2evenALTV  46347  6even  46366  8even  46368  6gbe  46426  7gbow  46427  8gbe  46428  9gbo  46429  11gbo  46430  uspgrsprf1  46512  1odd  46568  nnsgrp  46574  rngmgpf  46640  0even  46783  2even  46785  2zrngamgm  46791  2zrngasgrp  46792  2zrngamnd  46793  2zrngagrp  46795  2zrngmsgrp  46799  zlmodzxzldeplem3  47137  lvecpsslmod  47142  ldepsnlinc  47143  blennngt2o2  47232  blennn0e2  47234  ackval42  47336  rrx2xpref1o  47358  rrx2plordisom  47363  sepfsepc  47514  setrec2lem2  47693  aacllem  47802