Theorem mpbir2an 942

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 940	. 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  1175  euequ1  2121  eqssi  3173  elini  3321  dtruarb  4193  opnzi  4237  so0  4328  we0  4363  ord0  4393  ordon  4487  onsucelsucexmidlem1  4529  regexmidlemm  4533  ordpwsucexmid  4571  reg3exmidlemwe  4580  ordom  4608  funi  5250  funcnvsn  5263  funinsn  5267  fnresi  5335  fn0  5337  f0  5408  fconst  5413  f10  5497  f1o0  5500  f1oi  5501  f1osn  5503  isoid  5813  iso0  5820  acexmidlem2  5874  fo1st  6160  fo2nd  6161  iordsmo  6300  tfrlem7  6320  tfrexlem  6337  mapsnf1o2  6698  1domsn  6821  inresflem  7061  0ct  7108  infnninf  7124  infnninfOLD  7125  exmidonfinlem  7194  exmidaclem  7209  pw1on  7227  sucpw1nel3  7234  1pi  7316  prarloclemcalc  7503  ltsopr  7597  ltsosr  7765  cnm  7833  axicn  7864  axaddf  7869  axmulf  7870  nnindnn  7894  ltso  8037  negiso  8914  nnind  8937  0z  9266  dfuzi  9365  cnref1o  9652  elrpii  9658  xrltso  9798  0e0icopnf  9981  0e0iccpnf  9982  fz0to4untppr  10126  fldiv4p1lem1div2  10307  expcl2lemap  10534  expclzaplem  10546  expge0  10558  expge1  10559  xrnegiso  11272  fclim  11304  eff2  11690  reeff1  11710  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  egt2lt3  11789  halfleoddlt  11901  2prm  12129  3prm  12130  1arith  12367  setsslnid  12516  xpsff1o  12773  isabli  13108  mgpf  13199  zringnzr  13531  fntopon  13563  istpsi  13578  ismeti  13885  tgqioo  14086  addcncntoplem  14090  divcnap  14094  abscncf  14111  recncf  14112  imcncf  14113  cjcncf  14114  dveflem  14226  reeff1o  14233  reefiso  14237  ioocosf1o  14314  lgslem2  14441  lgsfcl2  14446  lgsne0  14478  ex-fl  14516  bj-indint  14722  bj-omord  14751  012of  14784  2o01f  14785  0nninf  14792  peano4nninf  14794  taupi  14860