Theorem mpbir2an 927

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 925	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 145	1 |- ph

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3pm3.2i  1160  euequ1  2101  eqssi  3144  elini  3292  dtruarb  4155  opnzi  4198  so0  4289  we0  4324  ord0  4354  ordon  4448  onsucelsucexmidlem1  4490  regexmidlemm  4494  ordpwsucexmid  4532  reg3exmidlemwe  4541  ordom  4569  funi  5205  funcnvsn  5218  funinsn  5222  fnresi  5290  fn0  5292  f0  5363  fconst  5368  f10  5451  f1o0  5454  f1oi  5455  f1osn  5457  isoid  5763  iso0  5770  acexmidlem2  5824  fo1st  6108  fo2nd  6109  iordsmo  6247  tfrlem7  6267  tfrexlem  6284  mapsnf1o2  6644  1domsn  6767  inresflem  7007  0ct  7054  infnninf  7070  infnninfOLD  7071  exmidonfinlem  7131  exmidaclem  7146  pw1on  7164  sucpw1nel3  7171  1pi  7238  prarloclemcalc  7425  ltsopr  7519  ltsosr  7687  cnm  7755  axicn  7786  axaddf  7791  axmulf  7792  nnindnn  7816  ltso  7958  negiso  8832  nnind  8855  0z  9184  dfuzi  9280  cnref1o  9566  elrpii  9570  xrltso  9710  0e0icopnf  9890  0e0iccpnf  9891  fz0to4untppr  10033  fldiv4p1lem1div2  10214  expcl2lemap  10441  expclzaplem  10453  expge0  10465  expge1  10466  xrnegiso  11171  fclim  11203  eff2  11589  reeff1  11609  ef01bndlem  11665  sin01bnd  11666  cos01bnd  11667  sin01gt0  11670  egt2lt3  11688  halfleoddlt  11798  2prm  12020  3prm  12021  setsslnid  12337  fntopon  12518  istpsi  12533  ismeti  12842  tgqioo  13043  addcncntoplem  13047  divcnap  13051  abscncf  13068  recncf  13069  imcncf  13070  cjcncf  13071  dveflem  13183  reeff1o  13190  reefiso  13194  ioocosf1o  13271  ex-fl  13398  bj-indint  13603  bj-omord  13632  012of  13664  2o01f  13665  0nninf  13673  peano4nninf  13675  taupi  13738