Theorem mpbir2an 950

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 948	. 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  1201  euequ1  2175  eqssi  3243  elini  3391  dtruarb  4281  opnzi  4327  so0  4423  we0  4458  ord0  4488  ordon  4584  onsucelsucexmidlem1  4626  regexmidlemm  4630  ordpwsucexmid  4668  reg3exmidlemwe  4677  ordom  4705  funi  5358  funcnvsn  5375  funinsn  5379  fnresi  5450  fn0  5452  f0  5527  fconst  5532  f10  5618  f1o0  5622  f1oi  5623  f1osn  5625  funopsn  5830  isoid  5951  iso0  5958  acexmidlem2  6015  fo1st  6320  fo2nd  6321  iordsmo  6463  tfrlem7  6483  tfrexlem  6500  mapsnf1o2  6865  1domsn  7001  inresflem  7259  0ct  7306  infnninf  7323  infnninfOLD  7324  exmidonfinlem  7404  exmidaclem  7423  pw1on  7444  sucpw1nel3  7451  1pi  7535  prarloclemcalc  7722  ltsopr  7816  ltsosr  7984  cnm  8052  axicn  8083  axaddf  8088  axmulf  8089  nnindnn  8113  mpomulf  8169  ltso  8257  negiso  9135  nnind  9159  0z  9490  dfuzi  9590  cnref1o  9885  elrpii  9891  xrltso  10031  0e0icopnf  10214  0e0iccpnf  10215  fz0to4untppr  10359  fldiv4p1lem1div2  10566  expcl2lemap  10814  expclzaplem  10826  expge0  10838  expge1  10839  xrnegiso  11840  fclim  11872  eff2  12259  reeff1  12279  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  egt2lt3  12359  halfleoddlt  12473  2prm  12717  3prm  12718  1arith  12958  setsslnid  13152  xpsff1o  13450  isabli  13905  rngmgpf  13969  mgpf  14043  zringnzr  14635  fntopon  14767  istpsi  14782  ismeti  15089  cnfldms  15279  tgqioo  15298  addcncntoplem  15304  divcnap  15308  abscncf  15328  recncf  15329  imcncf  15330  cjcncf  15331  maxcncf  15358  mincncf  15359  dveflem  15469  reeff1o  15516  reefiso  15520  ioocosf1o  15597  lgslem2  15749  lgsfcl2  15754  lgsne0  15786  2lgslem1b  15837  umgrbien  15980  konigsberglem1  16358  konigsberglem4  16361  ex-fl  16368  bj-indint  16577  bj-omord  16606  012of  16643  2o01f  16644  0nninf  16657  peano4nninf  16659  taupi  16729