Theorem mpbir2an 944

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 942	. 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  1177  euequ1  2140  eqssi  3200  elini  3348  dtruarb  4225  opnzi  4269  so0  4362  we0  4397  ord0  4427  ordon  4523  onsucelsucexmidlem1  4565  regexmidlemm  4569  ordpwsucexmid  4607  reg3exmidlemwe  4616  ordom  4644  funi  5291  funcnvsn  5304  funinsn  5308  fnresi  5378  fn0  5380  f0  5451  fconst  5456  f10  5541  f1o0  5544  f1oi  5545  f1osn  5547  isoid  5860  iso0  5867  acexmidlem2  5922  fo1st  6224  fo2nd  6225  iordsmo  6364  tfrlem7  6384  tfrexlem  6401  mapsnf1o2  6764  1domsn  6887  inresflem  7135  0ct  7182  infnninf  7199  infnninfOLD  7200  exmidonfinlem  7272  exmidaclem  7291  pw1on  7309  sucpw1nel3  7316  1pi  7399  prarloclemcalc  7586  ltsopr  7680  ltsosr  7848  cnm  7916  axicn  7947  axaddf  7952  axmulf  7953  nnindnn  7977  mpomulf  8033  ltso  8121  negiso  8999  nnind  9023  0z  9354  dfuzi  9453  cnref1o  9742  elrpii  9748  xrltso  9888  0e0icopnf  10071  0e0iccpnf  10072  fz0to4untppr  10216  fldiv4p1lem1div2  10412  expcl2lemap  10660  expclzaplem  10672  expge0  10684  expge1  10685  xrnegiso  11444  fclim  11476  eff2  11862  reeff1  11882  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  sin01gt0  11944  egt2lt3  11962  halfleoddlt  12076  2prm  12320  3prm  12321  1arith  12561  setsslnid  12755  xpsff1o  13051  isabli  13506  rngmgpf  13569  mgpf  13643  zringnzr  14234  fntopon  14344  istpsi  14359  ismeti  14666  cnfldms  14856  tgqioo  14875  addcncntoplem  14881  divcnap  14885  abscncf  14905  recncf  14906  imcncf  14907  cjcncf  14908  maxcncf  14935  mincncf  14936  dveflem  15046  reeff1o  15093  reefiso  15097  ioocosf1o  15174  lgslem2  15326  lgsfcl2  15331  lgsne0  15363  2lgslem1b  15414  ex-fl  15455  bj-indint  15661  bj-omord  15690  012of  15724  2o01f  15725  0nninf  15735  peano4nninf  15737  taupi  15804