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  4330  opnzi  4377  so0  4473  we0  4508  ord0  4538  ordon  4635  onsucelsucexmidlem1  4677  regexmidlemm  4681  ordpwsucexmid  4719  reg3exmidlemwe  4728  ordom  4756  funi  5412  funcnvsn  5429  funinsn  5433  fnresi  5504  fn0  5506  f0  5586  fconst  5591  f10  5677  f1o0  5681  f1oi  5682  f1osn  5684  funopsn  5894  isoid  6019  iso0  6026  rinvf1o  6038  acexmidlem2  6085  fo1st  6395  fo2nd  6396  iordsmo  6572  tfrlem7  6592  tfrexlem  6609  mapsnf1o2  6982  1domsn  7119  inresflem  7406  0ct  7453  infnninf  7470  infnninfOLD  7471  exmidonfinlem  7551  exmidaclem  7570  pw1on  7591  sucpw1nel3  7598  1pi  7688  prarloclemcalc  7875  ltsopr  7969  ltsosr  8137  cnm  8205  axicn  8236  axaddf  8241  axmulf  8242  nnindnn  8266  mpomulf  8322  ltso  8409  negiso  9293  nnind  9329  0z  9666  dfuzi  9767  cnref1o  10068  elrpii  10074  xrltso  10215  0e0icopnf  10398  0e0iccpnf  10399  fz0to4untppr  10548  fldiv4p1lem1div2  10761  expcl2lemap  11009  expclzaplem  11021  expge0  11033  expge1  11034  xrnegiso  12053  fclim  12085  eff2  12472  reeff1  12492  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sin01gt0  12554  egt2lt3  12572  halfleoddlt  12686  2prm  12930  3prm  12931  1arith  13175  prmlem1a  13250  ballotfilemonn  13279  ballotfilem2  13286  setsslnid  13462  xpsff1o  13729  isabli  14193  rngmgpf  14343  mgpf  14422  zringnzr  15046  fntopon  15250  istpsi  15265  ismeti  15572  cnfldms  15762  tgqioo  15781  addcncntoplem  15787  divcnap  15791  abscncf  15811  recncf  15812  imcncf  15813  cjcncf  15814  maxcncf  15841  mincncf  15842  dveflem  15952  reeff1o  15999  reefiso  16003  ioocosf1o  16082  efnnfsumcl  16239  efchtqdvds  16265  ppiqub  16293  lgslem2  16325  lgsfcl2  16330  lgsne0  16362  2lgslem1b  16413  umgrbien  16556  konigsberglem1  16934  konigsberglem4  16937  ex-fl  16944  bj-indint  17162  bj-omord  17191  012of  17228  2o01f  17229  0nninf  17253  peano4nninf  17255  taupi  17330