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  2140  eqssi  3200  elini  3348  dtruarb  4225  opnzi  4269  so0  4362  we0  4397  ord0  4427  ordon  4523  onsucelsucexmidlem1  4565  regexmidlemm  4569  ordpwsucexmid  4607  reg3exmidlemwe  4616  ordom  4644  funi  5291  funcnvsn  5304  funinsn  5308  fnresi  5378  fn0  5380  f0  5451  fconst  5456  f10  5541  f1o0  5544  f1oi  5545  f1osn  5547  isoid  5860  iso0  5867  acexmidlem2  5922  fo1st  6224  fo2nd  6225  iordsmo  6364  tfrlem7  6384  tfrexlem  6401  mapsnf1o2  6764  1domsn  6887  inresflem  7135  0ct  7182  infnninf  7199  infnninfOLD  7200  exmidonfinlem  7274  exmidaclem  7293  pw1on  7311  sucpw1nel3  7318  1pi  7401  prarloclemcalc  7588  ltsopr  7682  ltsosr  7850  cnm  7918  axicn  7949  axaddf  7954  axmulf  7955  nnindnn  7979  mpomulf  8035  ltso  8123  negiso  9001  nnind  9025  0z  9356  dfuzi  9455  cnref1o  9744  elrpii  9750  xrltso  9890  0e0icopnf  10073  0e0iccpnf  10074  fz0to4untppr  10218  fldiv4p1lem1div2  10414  expcl2lemap  10662  expclzaplem  10674  expge0  10686  expge1  10687  xrnegiso  11446  fclim  11478  eff2  11864  reeff1  11884  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sin01gt0  11946  egt2lt3  11964  halfleoddlt  12078  2prm  12322  3prm  12323  1arith  12563  setsslnid  12757  xpsff1o  13053  isabli  13508  rngmgpf  13571  mgpf  13645  zringnzr  14236  fntopon  14368  istpsi  14383  ismeti  14690  cnfldms  14880  tgqioo  14899  addcncntoplem  14905  divcnap  14909  abscncf  14929  recncf  14930  imcncf  14931  cjcncf  14932  maxcncf  14959  mincncf  14960  dveflem  15070  reeff1o  15117  reefiso  15121  ioocosf1o  15198  lgslem2  15350  lgsfcl2  15355  lgsne0  15387  2lgslem1b  15438  ex-fl  15479  bj-indint  15685  bj-omord  15714  012of  15748  2o01f  15749  0nninf  15759  peano4nninf  15761  taupi  15830