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  3241  elini  3389  dtruarb  4279  opnzi  4325  so0  4421  we0  4456  ord0  4486  ordon  4582  onsucelsucexmidlem1  4624  regexmidlemm  4628  ordpwsucexmid  4666  reg3exmidlemwe  4675  ordom  4703  funi  5356  funcnvsn  5372  funinsn  5376  fnresi  5447  fn0  5449  f0  5524  fconst  5529  f10  5614  f1o0  5618  f1oi  5619  f1osn  5621  funopsn  5825  isoid  5946  iso0  5953  acexmidlem2  6010  fo1st  6315  fo2nd  6316  iordsmo  6458  tfrlem7  6478  tfrexlem  6495  mapsnf1o2  6860  1domsn  6996  inresflem  7250  0ct  7297  infnninf  7314  infnninfOLD  7315  exmidonfinlem  7394  exmidaclem  7413  pw1on  7434  sucpw1nel3  7441  1pi  7525  prarloclemcalc  7712  ltsopr  7806  ltsosr  7974  cnm  8042  axicn  8073  axaddf  8078  axmulf  8079  nnindnn  8103  mpomulf  8159  ltso  8247  negiso  9125  nnind  9149  0z  9480  dfuzi  9580  cnref1o  9875  elrpii  9881  xrltso  10021  0e0icopnf  10204  0e0iccpnf  10205  fz0to4untppr  10349  fldiv4p1lem1div2  10555  expcl2lemap  10803  expclzaplem  10815  expge0  10827  expge1  10828  xrnegiso  11813  fclim  11845  eff2  12231  reeff1  12251  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  egt2lt3  12331  halfleoddlt  12445  2prm  12689  3prm  12690  1arith  12930  setsslnid  13124  xpsff1o  13422  isabli  13877  rngmgpf  13940  mgpf  14014  zringnzr  14606  fntopon  14738  istpsi  14753  ismeti  15060  cnfldms  15250  tgqioo  15269  addcncntoplem  15275  divcnap  15279  abscncf  15299  recncf  15300  imcncf  15301  cjcncf  15302  maxcncf  15329  mincncf  15330  dveflem  15440  reeff1o  15487  reefiso  15491  ioocosf1o  15568  lgslem2  15720  lgsfcl2  15725  lgsne0  15757  2lgslem1b  15808  umgrbien  15951  ex-fl  16257  bj-indint  16462  bj-omord  16491  012of  16528  2o01f  16529  0nninf  16542  peano4nninf  16544  taupi  16613