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  4275  opnzi  4321  so0  4417  we0  4452  ord0  4482  ordon  4578  onsucelsucexmidlem1  4620  regexmidlemm  4624  ordpwsucexmid  4662  reg3exmidlemwe  4671  ordom  4699  funi  5350  funcnvsn  5366  funinsn  5370  fnresi  5441  fn0  5443  f0  5518  fconst  5523  f10  5608  f1o0  5612  f1oi  5613  f1osn  5615  funopsn  5819  isoid  5940  iso0  5947  acexmidlem2  6004  fo1st  6309  fo2nd  6310  iordsmo  6449  tfrlem7  6469  tfrexlem  6486  mapsnf1o2  6851  1domsn  6984  inresflem  7238  0ct  7285  infnninf  7302  infnninfOLD  7303  exmidonfinlem  7382  exmidaclem  7401  pw1on  7422  sucpw1nel3  7429  1pi  7513  prarloclemcalc  7700  ltsopr  7794  ltsosr  7962  cnm  8030  axicn  8061  axaddf  8066  axmulf  8067  nnindnn  8091  mpomulf  8147  ltso  8235  negiso  9113  nnind  9137  0z  9468  dfuzi  9568  cnref1o  9858  elrpii  9864  xrltso  10004  0e0icopnf  10187  0e0iccpnf  10188  fz0to4untppr  10332  fldiv4p1lem1div2  10537  expcl2lemap  10785  expclzaplem  10797  expge0  10809  expge1  10810  xrnegiso  11788  fclim  11820  eff2  12206  reeff1  12226  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  sin01gt0  12288  egt2lt3  12306  halfleoddlt  12420  2prm  12664  3prm  12665  1arith  12905  setsslnid  13099  xpsff1o  13397  isabli  13852  rngmgpf  13915  mgpf  13989  zringnzr  14581  fntopon  14713  istpsi  14728  ismeti  15035  cnfldms  15225  tgqioo  15244  addcncntoplem  15250  divcnap  15254  abscncf  15274  recncf  15275  imcncf  15276  cjcncf  15277  maxcncf  15304  mincncf  15305  dveflem  15415  reeff1o  15462  reefiso  15466  ioocosf1o  15543  lgslem2  15695  lgsfcl2  15700  lgsne0  15732  2lgslem1b  15783  umgrbien  15925  ex-fl  16144  bj-indint  16349  bj-omord  16378  012of  16416  2o01f  16417  0nninf  16430  peano4nninf  16432  taupi  16501