Theorem mpbir2an 951

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 949	. 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  1202  euequ1  2178  eqssi  3258  elini  3407  dtruarb  4309  opnzi  4356  so0  4452  we0  4487  ord0  4517  ordon  4613  onsucelsucexmidlem1  4655  regexmidlemm  4659  ordpwsucexmid  4697  reg3exmidlemwe  4706  ordom  4734  funi  5389  funcnvsn  5406  funinsn  5410  fnresi  5481  fn0  5483  f0  5563  fconst  5568  f10  5654  f1o0  5658  f1oi  5659  f1osn  5661  funopsn  5865  isoid  5989  iso0  5996  rinvf1o  6008  acexmidlem2  6055  fo1st  6364  fo2nd  6365  iordsmo  6541  tfrlem7  6561  tfrexlem  6578  mapsnf1o2  6944  1domsn  7081  inresflem  7364  0ct  7411  infnninf  7428  infnninfOLD  7429  exmidonfinlem  7509  exmidaclem  7528  pw1on  7549  sucpw1nel3  7556  1pi  7646  prarloclemcalc  7833  ltsopr  7927  ltsosr  8095  cnm  8163  axicn  8194  axaddf  8199  axmulf  8200  nnindnn  8224  mpomulf  8280  ltso  8367  negiso  9246  nnind  9270  0z  9605  dfuzi  9706  cnref1o  10001  elrpii  10007  xrltso  10148  0e0icopnf  10331  0e0iccpnf  10332  fz0to4untppr  10480  fldiv4p1lem1div2  10689  expcl2lemap  10937  expclzaplem  10949  expge0  10961  expge1  10962  xrnegiso  11972  fclim  12004  eff2  12391  reeff1  12411  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  egt2lt3  12491  halfleoddlt  12605  2prm  12849  3prm  12850  1arith  13090  ballotfilemonn  13165  ballotfilem2  13172  setsslnid  13348  xpsff1o  13613  isabli  14053  rngmgpf  14176  mgpf  14254  zringnzr  14876  fntopon  15015  istpsi  15030  ismeti  15337  cnfldms  15527  tgqioo  15546  addcncntoplem  15552  divcnap  15556  abscncf  15576  recncf  15577  imcncf  15578  cjcncf  15579  maxcncf  15606  mincncf  15607  dveflem  15717  reeff1o  15764  reefiso  15768  ioocosf1o  15845  lgslem2  16000  lgsfcl2  16005  lgsne0  16037  2lgslem1b  16088  umgrbien  16231  konigsberglem1  16609  konigsberglem4  16612  ex-fl  16619  bj-indint  16827  bj-omord  16856  012of  16893  2o01f  16894  0nninf  16908  peano4nninf  16910  taupi  16985