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  6573  tfrlem7  6593  tfrexlem  6610  mapsnf1o2  6984  1domsn  7121  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  9664  dfuzi  9766  cnref1o  10067  elrpii  10073  xrltso  10214  0e0icopnf  10397  0e0iccpnf  10398  fz0to4untppr  10547  fldiv4p1lem1div2  10760  expcl2lemap  11008  expclzaplem  11020  expge0  11032  expge1  11033  xrnegiso  12052  fclim  12084  eff2  12471  reeff1  12491  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  sin01gt0  12553  egt2lt3  12571  halfleoddlt  12685  2prm  12929  3prm  12930  1arith  13174  prmlem1a  13249  ballotfilemonn  13278  ballotfilem2  13285  setsslnid  13461  xpsff1o  13728  isabli  14192  rngmgpf  14342  mgpf  14421  zringnzr  15045  fntopon  15267  istpsi  15282  ismeti  15589  cnfldms  15779  tgqioo  15798  addcncntoplem  15804  divcnap  15808  abscncf  15828  recncf  15829  imcncf  15830  cjcncf  15831  maxcncf  15858  mincncf  15859  dveflem  15969  reeff1o  16016  reefiso  16020  ioocosf1o  16099  efnnfsumcl  16256  efchtqdvds  16282  ppiqub  16310  lgslem2  16342  lgsfcl2  16347  lgsne0  16379  2lgslem1b  16430  umgrbien  16573  konigsberglem1  16951  konigsberglem4  16954  ex-fl  16961  bj-indint  17179  bj-omord  17208  012of  17245  2o01f  17246  0nninf  17270  peano4nninf  17272  taupi  17347