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  2148  eqssi  3208  elini  3356  dtruarb  4234  opnzi  4278  so0  4371  we0  4406  ord0  4436  ordon  4532  onsucelsucexmidlem1  4574  regexmidlemm  4578  ordpwsucexmid  4616  reg3exmidlemwe  4625  ordom  4653  funi  5300  funcnvsn  5313  funinsn  5317  fnresi  5387  fn0  5389  f0  5460  fconst  5465  f10  5550  f1o0  5553  f1oi  5554  f1osn  5556  isoid  5869  iso0  5876  acexmidlem2  5931  fo1st  6233  fo2nd  6234  iordsmo  6373  tfrlem7  6393  tfrexlem  6410  mapsnf1o2  6773  1domsn  6896  inresflem  7144  0ct  7191  infnninf  7208  infnninfOLD  7209  exmidonfinlem  7283  exmidaclem  7302  pw1on  7320  sucpw1nel3  7327  1pi  7410  prarloclemcalc  7597  ltsopr  7691  ltsosr  7859  cnm  7927  axicn  7958  axaddf  7963  axmulf  7964  nnindnn  7988  mpomulf  8044  ltso  8132  negiso  9010  nnind  9034  0z  9365  dfuzi  9465  cnref1o  9754  elrpii  9760  xrltso  9900  0e0icopnf  10083  0e0iccpnf  10084  fz0to4untppr  10228  fldiv4p1lem1div2  10429  expcl2lemap  10677  expclzaplem  10689  expge0  10701  expge1  10702  xrnegiso  11492  fclim  11524  eff2  11910  reeff1  11930  ef01bndlem  11986  sin01bnd  11987  cos01bnd  11988  sin01gt0  11992  egt2lt3  12010  halfleoddlt  12124  2prm  12368  3prm  12369  1arith  12609  setsslnid  12803  xpsff1o  13099  isabli  13554  rngmgpf  13617  mgpf  13691  zringnzr  14282  fntopon  14414  istpsi  14429  ismeti  14736  cnfldms  14926  tgqioo  14945  addcncntoplem  14951  divcnap  14955  abscncf  14975  recncf  14976  imcncf  14977  cjcncf  14978  maxcncf  15005  mincncf  15006  dveflem  15116  reeff1o  15163  reefiso  15167  ioocosf1o  15244  lgslem2  15396  lgsfcl2  15401  lgsne0  15433  2lgslem1b  15484  ex-fl  15525  bj-indint  15731  bj-omord  15760  012of  15794  2o01f  15795  0nninf  15805  peano4nninf  15807  taupi  15876