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  4191  opnzi  4235  so0  4326  we0  4361  ord0  4391  ordon  4485  onsucelsucexmidlem1  4527  regexmidlemm  4531  ordpwsucexmid  4569  reg3exmidlemwe  4578  ordom  4606  funi  5248  funcnvsn  5261  funinsn  5265  fnresi  5333  fn0  5335  f0  5406  fconst  5411  f10  5495  f1o0  5498  f1oi  5499  f1osn  5501  isoid  5810  iso0  5817  acexmidlem2  5871  fo1st  6157  fo2nd  6158  iordsmo  6297  tfrlem7  6317  tfrexlem  6334  mapsnf1o2  6695  1domsn  6818  inresflem  7058  0ct  7105  infnninf  7121  infnninfOLD  7122  exmidonfinlem  7191  exmidaclem  7206  pw1on  7224  sucpw1nel3  7231  1pi  7313  prarloclemcalc  7500  ltsopr  7594  ltsosr  7762  cnm  7830  axicn  7861  axaddf  7866  axmulf  7867  nnindnn  7891  ltso  8034  negiso  8911  nnind  8934  0z  9263  dfuzi  9362  cnref1o  9649  elrpii  9655  xrltso  9795  0e0icopnf  9978  0e0iccpnf  9979  fz0to4untppr  10123  fldiv4p1lem1div2  10304  expcl2lemap  10531  expclzaplem  10543  expge0  10555  expge1  10556  xrnegiso  11269  fclim  11301  eff2  11687  reeff1  11707  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  egt2lt3  11786  halfleoddlt  11898  2prm  12126  3prm  12127  1arith  12364  setsslnid  12513  xpsff1o  12767  isabli  13101  mgpf  13192  zringnzr  13462  fntopon  13494  istpsi  13509  ismeti  13816  tgqioo  14017  addcncntoplem  14021  divcnap  14025  abscncf  14042  recncf  14043  imcncf  14044  cjcncf  14045  dveflem  14157  reeff1o  14164  reefiso  14168  ioocosf1o  14245  lgslem2  14372  lgsfcl2  14377  lgsne0  14409  ex-fl  14447  bj-indint  14653  bj-omord  14682  012of  14715  2o01f  14716  0nninf  14723  peano4nninf  14725  taupi  14790