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  9287  nnind  9322  0z  9659  dfuzi  9760  cnref1o  10061  elrpii  10067  xrltso  10208  0e0icopnf  10391  0e0iccpnf  10392  fz0to4untppr  10541  fldiv4p1lem1div2  10753  expcl2lemap  11001  expclzaplem  11013  expge0  11025  expge1  11026  xrnegiso  12044  fclim  12076  eff2  12463  reeff1  12483  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  egt2lt3  12563  halfleoddlt  12677  2prm  12921  3prm  12922  1arith  13166  prmlem1a  13241  ballotfilemonn  13270  ballotfilem2  13277  setsslnid  13453  xpsff1o  13719  isabli  14152  rngmgpf  14285  mgpf  14364  zringnzr  14986  fntopon  15174  istpsi  15189  ismeti  15496  cnfldms  15686  tgqioo  15705  addcncntoplem  15711  divcnap  15715  abscncf  15735  recncf  15736  imcncf  15737  cjcncf  15738  maxcncf  15765  mincncf  15766  dveflem  15876  reeff1o  15923  reefiso  15927  ioocosf1o  16005  ppiqub  16194  lgslem2  16218  lgsfcl2  16223  lgsne0  16255  2lgslem1b  16306  umgrbien  16449  konigsberglem1  16827  konigsberglem4  16830  ex-fl  16837  bj-indint  17055  bj-omord  17084  012of  17121  2o01f  17122  0nninf  17145  peano4nninf  17147  taupi  17221