Theorem mpbir2an 944

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 942	. 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  1177  euequ1  2137  eqssi  3196  elini  3344  dtruarb  4221  opnzi  4265  so0  4358  we0  4393  ord0  4423  ordon  4519  onsucelsucexmidlem1  4561  regexmidlemm  4565  ordpwsucexmid  4603  reg3exmidlemwe  4612  ordom  4640  funi  5287  funcnvsn  5300  funinsn  5304  fnresi  5372  fn0  5374  f0  5445  fconst  5450  f10  5535  f1o0  5538  f1oi  5539  f1osn  5541  isoid  5854  iso0  5861  acexmidlem2  5916  fo1st  6212  fo2nd  6213  iordsmo  6352  tfrlem7  6372  tfrexlem  6389  mapsnf1o2  6752  1domsn  6875  inresflem  7121  0ct  7168  infnninf  7185  infnninfOLD  7186  exmidonfinlem  7255  exmidaclem  7270  pw1on  7288  sucpw1nel3  7295  1pi  7377  prarloclemcalc  7564  ltsopr  7658  ltsosr  7826  cnm  7894  axicn  7925  axaddf  7930  axmulf  7931  nnindnn  7955  mpomulf  8011  ltso  8099  negiso  8976  nnind  9000  0z  9331  dfuzi  9430  cnref1o  9719  elrpii  9725  xrltso  9865  0e0icopnf  10048  0e0iccpnf  10049  fz0to4untppr  10193  fldiv4p1lem1div2  10377  expcl2lemap  10625  expclzaplem  10637  expge0  10649  expge1  10650  xrnegiso  11408  fclim  11440  eff2  11826  reeff1  11846  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sin01gt0  11908  egt2lt3  11926  halfleoddlt  12038  2prm  12268  3prm  12269  1arith  12508  setsslnid  12673  xpsff1o  12935  isabli  13373  rngmgpf  13436  mgpf  13510  zringnzr  14101  fntopon  14203  istpsi  14218  ismeti  14525  cnfldms  14715  tgqioo  14734  addcncntoplem  14740  divcnap  14744  abscncf  14764  recncf  14765  imcncf  14766  cjcncf  14767  maxcncf  14794  mincncf  14795  dveflem  14905  reeff1o  14949  reefiso  14953  ioocosf1o  15030  lgslem2  15158  lgsfcl2  15163  lgsne0  15195  2lgslem1b  15246  ex-fl  15287  bj-indint  15493  bj-omord  15522  012of  15556  2o01f  15557  0nninf  15564  peano4nninf  15566  taupi  15633