Theorem mpbir2an 955

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 953	. 2 |- ( ph <-> ch )
5	1, 4	mpbir 146	1 |- ph

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3pm3.2i  1206  euequ1  2182  eqssi  3264  elini  3413  dtruarb  4328  opnzi  4375  so0  4471  we0  4506  ord0  4536  ordon  4633  onsucelsucexmidlem1  4675  regexmidlemm  4679  ordpwsucexmid  4717  reg3exmidlemwe  4726  ordom  4754  funi  5409  funcnvsn  5426  funinsn  5430  fnresi  5501  fn0  5503  f0  5583  fconst  5588  f10  5674  f1o0  5678  f1oi  5679  f1osn  5681  funopsn  5891  isoid  6016  iso0  6023  rinvf1o  6035  acexmidlem2  6082  fo1st  6391  fo2nd  6392  iordsmo  6568  tfrlem7  6588  tfrexlem  6605  mapsnf1o2  6978  1domsn  7115  inresflem  7400  0ct  7447  infnninf  7464  infnninfOLD  7465  exmidonfinlem  7545  exmidaclem  7564  pw1on  7585  sucpw1nel3  7592  1pi  7682  prarloclemcalc  7869  ltsopr  7963  ltsosr  8131  cnm  8199  axicn  8230  axaddf  8235  axmulf  8236  nnindnn  8260  mpomulf  8316  ltso  8403  negiso  9285  nnind  9320  0z  9655  dfuzi  9756  cnref1o  10051  elrpii  10057  xrltso  10198  0e0icopnf  10381  0e0iccpnf  10382  fz0to4untppr  10531  fldiv4p1lem1div2  10740  expcl2lemap  10988  expclzaplem  11000  expge0  11012  expge1  11013  xrnegiso  12028  fclim  12060  eff2  12447  reeff1  12467  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sin01gt0  12529  egt2lt3  12547  halfleoddlt  12661  2prm  12905  3prm  12906  1arith  13146  ballotfilemonn  13221  ballotfilem2  13228  setsslnid  13404  xpsff1o  13670  isabli  14103  rngmgpf  14236  mgpf  14315  zringnzr  14937  fntopon  15125  istpsi  15140  ismeti  15447  cnfldms  15637  tgqioo  15656  addcncntoplem  15662  divcnap  15666  abscncf  15686  recncf  15687  imcncf  15688  cjcncf  15689  maxcncf  15716  mincncf  15717  dveflem  15827  reeff1o  15874  reefiso  15878  ioocosf1o  15955  lgslem2  16120  lgsfcl2  16125  lgsne0  16157  2lgslem1b  16208  umgrbien  16351  konigsberglem1  16729  konigsberglem4  16732  ex-fl  16739  bj-indint  16957  bj-omord  16986  012of  17023  2o01f  17024  0nninf  17047  peano4nninf  17049  taupi  17123