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  4277  opnzi  4323  so0  4419  we0  4454  ord0  4484  ordon  4580  onsucelsucexmidlem1  4622  regexmidlemm  4626  ordpwsucexmid  4664  reg3exmidlemwe  4673  ordom  4701  funi  5354  funcnvsn  5370  funinsn  5374  fnresi  5445  fn0  5447  f0  5522  fconst  5527  f10  5612  f1o0  5616  f1oi  5617  f1osn  5619  funopsn  5823  isoid  5944  iso0  5951  acexmidlem2  6008  fo1st  6313  fo2nd  6314  iordsmo  6456  tfrlem7  6476  tfrexlem  6493  mapsnf1o2  6858  1domsn  6994  inresflem  7248  0ct  7295  infnninf  7312  infnninfOLD  7313  exmidonfinlem  7392  exmidaclem  7411  pw1on  7432  sucpw1nel3  7439  1pi  7523  prarloclemcalc  7710  ltsopr  7804  ltsosr  7972  cnm  8040  axicn  8071  axaddf  8076  axmulf  8077  nnindnn  8101  mpomulf  8157  ltso  8245  negiso  9123  nnind  9147  0z  9478  dfuzi  9578  cnref1o  9873  elrpii  9879  xrltso  10019  0e0icopnf  10202  0e0iccpnf  10203  fz0to4untppr  10347  fldiv4p1lem1div2  10553  expcl2lemap  10801  expclzaplem  10813  expge0  10825  expge1  10826  xrnegiso  11810  fclim  11842  eff2  12228  reeff1  12248  ef01bndlem  12304  sin01bnd  12305  cos01bnd  12306  sin01gt0  12310  egt2lt3  12328  halfleoddlt  12442  2prm  12686  3prm  12687  1arith  12927  setsslnid  13121  xpsff1o  13419  isabli  13874  rngmgpf  13937  mgpf  14011  zringnzr  14603  fntopon  14735  istpsi  14750  ismeti  15057  cnfldms  15247  tgqioo  15266  addcncntoplem  15272  divcnap  15276  abscncf  15296  recncf  15297  imcncf  15298  cjcncf  15299  maxcncf  15326  mincncf  15327  dveflem  15437  reeff1o  15484  reefiso  15488  ioocosf1o  15565  lgslem2  15717  lgsfcl2  15722  lgsne0  15754  2lgslem1b  15805  umgrbien  15947  ex-fl  16231  bj-indint  16436  bj-omord  16465  012of  16502  2o01f  16503  0nninf  16516  peano4nninf  16518  taupi  16587