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  3171  elini  3319  dtruarb  4190  opnzi  4234  so0  4325  we0  4360  ord0  4390  ordon  4484  onsucelsucexmidlem1  4526  regexmidlemm  4530  ordpwsucexmid  4568  reg3exmidlemwe  4577  ordom  4605  funi  5247  funcnvsn  5260  funinsn  5264  fnresi  5332  fn0  5334  f0  5405  fconst  5410  f10  5494  f1o0  5497  f1oi  5498  f1osn  5500  isoid  5808  iso0  5815  acexmidlem2  5869  fo1st  6155  fo2nd  6156  iordsmo  6295  tfrlem7  6315  tfrexlem  6332  mapsnf1o2  6693  1domsn  6816  inresflem  7056  0ct  7103  infnninf  7119  infnninfOLD  7120  exmidonfinlem  7189  exmidaclem  7204  pw1on  7222  sucpw1nel3  7229  1pi  7311  prarloclemcalc  7498  ltsopr  7592  ltsosr  7760  cnm  7828  axicn  7859  axaddf  7864  axmulf  7865  nnindnn  7889  ltso  8031  negiso  8908  nnind  8931  0z  9260  dfuzi  9359  cnref1o  9646  elrpii  9652  xrltso  9792  0e0icopnf  9975  0e0iccpnf  9976  fz0to4untppr  10119  fldiv4p1lem1div2  10300  expcl2lemap  10527  expclzaplem  10539  expge0  10551  expge1  10552  xrnegiso  11263  fclim  11295  eff2  11681  reeff1  11701  ef01bndlem  11757  sin01bnd  11758  cos01bnd  11759  sin01gt0  11762  egt2lt3  11780  halfleoddlt  11891  2prm  12119  3prm  12120  1arith  12357  setsslnid  12506  isabli  13034  mgpf  13125  zringnzr  13361  fntopon  13393  istpsi  13408  ismeti  13717  tgqioo  13918  addcncntoplem  13922  divcnap  13926  abscncf  13943  recncf  13944  imcncf  13945  cjcncf  13946  dveflem  14058  reeff1o  14065  reefiso  14069  ioocosf1o  14146  lgslem2  14273  lgsfcl2  14278  lgsne0  14310  ex-fl  14337  bj-indint  14543  bj-omord  14572  012of  14605  2o01f  14606  0nninf  14613  peano4nninf  14615  taupi  14680