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  2137  eqssi  3195  elini  3343  dtruarb  4220  opnzi  4264  so0  4357  we0  4392  ord0  4422  ordon  4518  onsucelsucexmidlem1  4560  regexmidlemm  4564  ordpwsucexmid  4602  reg3exmidlemwe  4611  ordom  4639  funi  5286  funcnvsn  5299  funinsn  5303  fnresi  5371  fn0  5373  f0  5444  fconst  5449  f10  5534  f1o0  5537  f1oi  5538  f1osn  5540  isoid  5853  iso0  5860  acexmidlem2  5915  fo1st  6210  fo2nd  6211  iordsmo  6350  tfrlem7  6370  tfrexlem  6387  mapsnf1o2  6750  1domsn  6873  inresflem  7119  0ct  7166  infnninf  7183  infnninfOLD  7184  exmidonfinlem  7253  exmidaclem  7268  pw1on  7286  sucpw1nel3  7293  1pi  7375  prarloclemcalc  7562  ltsopr  7656  ltsosr  7824  cnm  7892  axicn  7923  axaddf  7928  axmulf  7929  nnindnn  7953  mpomulf  8009  ltso  8097  negiso  8974  nnind  8998  0z  9328  dfuzi  9427  cnref1o  9716  elrpii  9722  xrltso  9862  0e0icopnf  10045  0e0iccpnf  10046  fz0to4untppr  10190  fldiv4p1lem1div2  10374  expcl2lemap  10622  expclzaplem  10634  expge0  10646  expge1  10647  xrnegiso  11405  fclim  11437  eff2  11823  reeff1  11843  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  sin01gt0  11905  egt2lt3  11923  halfleoddlt  12035  2prm  12265  3prm  12266  1arith  12505  setsslnid  12670  xpsff1o  12932  isabli  13370  rngmgpf  13433  mgpf  13507  zringnzr  14090  fntopon  14192  istpsi  14207  ismeti  14514  tgqioo  14715  addcncntoplem  14719  divcnap  14723  abscncf  14740  recncf  14741  imcncf  14742  cjcncf  14743  maxcncf  14769  mincncf  14770  dveflem  14872  reeff1o  14908  reefiso  14912  ioocosf1o  14989  lgslem2  15117  lgsfcl2  15122  lgsne0  15154  ex-fl  15217  bj-indint  15423  bj-omord  15452  012of  15486  2o01f  15487  0nninf  15494  peano4nninf  15496  taupi  15563