Theorem mpbir2an 926

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 924	. 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  1159  euequ1  2094  eqssi  3113  elini  3260  dtruarb  4115  opnzi  4157  so0  4248  we0  4283  ord0  4313  ordon  4402  onsucelsucexmidlem1  4443  regexmidlemm  4447  ordpwsucexmid  4485  reg3exmidlemwe  4493  ordom  4520  funi  5155  funcnvsn  5168  funinsn  5172  fnresi  5240  fn0  5242  f0  5313  fconst  5318  f10  5401  f1o0  5404  f1oi  5405  f1osn  5407  isoid  5711  iso0  5718  acexmidlem2  5771  fo1st  6055  fo2nd  6056  iordsmo  6194  tfrlem7  6214  tfrexlem  6231  mapsnf1o2  6590  1domsn  6713  inresflem  6945  0ct  6992  infnninf  7022  exmidonfinlem  7049  exmidaclem  7064  1pi  7123  prarloclemcalc  7310  ltsopr  7404  ltsosr  7572  cnm  7640  axicn  7671  axaddf  7676  axmulf  7677  nnindnn  7701  ltso  7842  negiso  8713  nnind  8736  0z  9065  dfuzi  9161  cnref1o  9440  elrpii  9444  xrltso  9582  0e0icopnf  9762  0e0iccpnf  9763  fldiv4p1lem1div2  10078  expcl2lemap  10305  expclzaplem  10317  expge0  10329  expge1  10330  xrnegiso  11031  fclim  11063  eff2  11386  reeff1  11407  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  egt2lt3  11486  halfleoddlt  11591  2prm  11808  3prm  11809  setsslnid  12010  fntopon  12191  istpsi  12206  ismeti  12515  tgqioo  12716  addcncntoplem  12720  divcnap  12724  abscncf  12741  recncf  12742  imcncf  12743  cjcncf  12744  dveflem  12855  ex-fl  12937  bj-indint  13129  bj-omord  13158  0nninf  13197  peano4nninf  13200  isomninnlem  13225  taupi  13239