Theorem mpbir2an 951

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbir2an.1	|- ps
mpbir2an.2	|- ch
mpbiran2an.1	|- ( ph <-> ( ps /\ ch ) )

Assertion

Ref	Expression
mpbir2an	|- ph

Proof of Theorem mpbir2an

Step	Hyp	Ref	Expression
1		mpbir2an.2	. 2 |- ch
2		mpbir2an.1	. . 3 |- ps
3		mpbiran2an.1	. . 3 |- ( ph <-> ( ps /\ ch ) )
4	2, 3	mpbiran 949	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 146	1 |- ph

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3pm3.2i  1202  euequ1  2175  eqssi  3244  elini  3393  dtruarb  4287  opnzi  4333  so0  4429  we0  4464  ord0  4494  ordon  4590  onsucelsucexmidlem1  4632  regexmidlemm  4636  ordpwsucexmid  4674  reg3exmidlemwe  4683  ordom  4711  funi  5365  funcnvsn  5382  funinsn  5386  fnresi  5457  fn0  5459  f0  5536  fconst  5541  f10  5627  f1o0  5631  f1oi  5632  f1osn  5634  funopsn  5838  isoid  5961  iso0  5968  acexmidlem2  6025  fo1st  6329  fo2nd  6330  iordsmo  6506  tfrlem7  6526  tfrexlem  6543  mapsnf1o2  6908  1domsn  7044  inresflem  7302  0ct  7349  infnninf  7366  infnninfOLD  7367  exmidonfinlem  7447  exmidaclem  7466  pw1on  7487  sucpw1nel3  7494  1pi  7578  prarloclemcalc  7765  ltsopr  7859  ltsosr  8027  cnm  8095  axicn  8126  axaddf  8131  axmulf  8132  nnindnn  8156  mpomulf  8212  ltso  8299  negiso  9177  nnind  9201  0z  9534  dfuzi  9634  cnref1o  9929  elrpii  9935  xrltso  10075  0e0icopnf  10258  0e0iccpnf  10259  fz0to4untppr  10404  fldiv4p1lem1div2  10611  expcl2lemap  10859  expclzaplem  10871  expge0  10883  expge1  10884  xrnegiso  11885  fclim  11917  eff2  12304  reeff1  12324  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  egt2lt3  12404  halfleoddlt  12518  2prm  12762  3prm  12763  1arith  13003  setsslnid  13197  xpsff1o  13495  isabli  13950  rngmgpf  14014  mgpf  14088  zringnzr  14681  fntopon  14818  istpsi  14833  ismeti  15140  cnfldms  15330  tgqioo  15349  addcncntoplem  15355  divcnap  15359  abscncf  15379  recncf  15380  imcncf  15381  cjcncf  15382  maxcncf  15409  mincncf  15410  dveflem  15520  reeff1o  15567  reefiso  15571  ioocosf1o  15648  lgslem2  15803  lgsfcl2  15808  lgsne0  15840  2lgslem1b  15891  umgrbien  16034  konigsberglem1  16412  konigsberglem4  16415  ex-fl  16422  bj-indint  16630  bj-omord  16659  012of  16696  2o01f  16697  0nninf  16713  peano4nninf  16715  taupi  16789