Theorem mpbir2an 948

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 946	. 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  1199  euequ1  2173  eqssi  3240  elini  3388  dtruarb  4274  opnzi  4320  so0  4416  we0  4451  ord0  4481  ordon  4577  onsucelsucexmidlem1  4619  regexmidlemm  4623  ordpwsucexmid  4661  reg3exmidlemwe  4670  ordom  4698  funi  5349  funcnvsn  5365  funinsn  5369  fnresi  5440  fn0  5442  f0  5515  fconst  5520  f10  5605  f1o0  5609  f1oi  5610  f1osn  5612  funopsn  5816  isoid  5933  iso0  5940  acexmidlem2  5997  fo1st  6301  fo2nd  6302  iordsmo  6441  tfrlem7  6461  tfrexlem  6478  mapsnf1o2  6841  1domsn  6974  inresflem  7223  0ct  7270  infnninf  7287  infnninfOLD  7288  exmidonfinlem  7367  exmidaclem  7386  pw1on  7407  sucpw1nel3  7414  1pi  7498  prarloclemcalc  7685  ltsopr  7779  ltsosr  7947  cnm  8015  axicn  8046  axaddf  8051  axmulf  8052  nnindnn  8076  mpomulf  8132  ltso  8220  negiso  9098  nnind  9122  0z  9453  dfuzi  9553  cnref1o  9842  elrpii  9848  xrltso  9988  0e0icopnf  10171  0e0iccpnf  10172  fz0to4untppr  10316  fldiv4p1lem1div2  10520  expcl2lemap  10768  expclzaplem  10780  expge0  10792  expge1  10793  xrnegiso  11768  fclim  11800  eff2  12186  reeff1  12206  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  sin01gt0  12268  egt2lt3  12286  halfleoddlt  12400  2prm  12644  3prm  12645  1arith  12885  setsslnid  13079  xpsff1o  13377  isabli  13832  rngmgpf  13895  mgpf  13969  zringnzr  14560  fntopon  14692  istpsi  14707  ismeti  15014  cnfldms  15204  tgqioo  15223  addcncntoplem  15229  divcnap  15233  abscncf  15253  recncf  15254  imcncf  15255  cjcncf  15256  maxcncf  15283  mincncf  15284  dveflem  15394  reeff1o  15441  reefiso  15445  ioocosf1o  15522  lgslem2  15674  lgsfcl2  15679  lgsne0  15711  2lgslem1b  15762  umgrbien  15904  ex-fl  16047  bj-indint  16252  bj-omord  16281  012of  16316  2o01f  16317  0nninf  16329  peano4nninf  16331  taupi  16400