Theorem mpbir2an 942

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 940	. 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  1175  euequ1  2121  eqssi  3171  elini  3319  dtruarb  4189  opnzi  4233  so0  4324  we0  4359  ord0  4389  ordon  4483  onsucelsucexmidlem1  4525  regexmidlemm  4529  ordpwsucexmid  4567  reg3exmidlemwe  4576  ordom  4604  funi  5245  funcnvsn  5258  funinsn  5262  fnresi  5330  fn0  5332  f0  5403  fconst  5408  f10  5492  f1o0  5495  f1oi  5496  f1osn  5498  isoid  5806  iso0  5813  acexmidlem2  5867  fo1st  6153  fo2nd  6154  iordsmo  6293  tfrlem7  6313  tfrexlem  6330  mapsnf1o2  6691  1domsn  6814  inresflem  7054  0ct  7101  infnninf  7117  infnninfOLD  7118  exmidonfinlem  7187  exmidaclem  7202  pw1on  7220  sucpw1nel3  7227  1pi  7309  prarloclemcalc  7496  ltsopr  7590  ltsosr  7758  cnm  7826  axicn  7857  axaddf  7862  axmulf  7863  nnindnn  7887  ltso  8029  negiso  8906  nnind  8929  0z  9258  dfuzi  9357  cnref1o  9644  elrpii  9650  xrltso  9790  0e0icopnf  9973  0e0iccpnf  9974  fz0to4untppr  10117  fldiv4p1lem1div2  10298  expcl2lemap  10525  expclzaplem  10537  expge0  10549  expge1  10550  xrnegiso  11261  fclim  11293  eff2  11679  reeff1  11699  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  sin01gt0  11760  egt2lt3  11778  halfleoddlt  11889  2prm  12117  3prm  12118  1arith  12355  setsslnid  12504  isabli  13003  mgpf  13094  fntopon  13304  istpsi  13319  ismeti  13628  tgqioo  13829  addcncntoplem  13833  divcnap  13837  abscncf  13854  recncf  13855  imcncf  13856  cjcncf  13857  dveflem  13969  reeff1o  13976  reefiso  13980  ioocosf1o  14057  lgslem2  14184  lgsfcl2  14189  lgsne0  14221  ex-fl  14248  bj-indint  14454  bj-omord  14483  012of  14516  2o01f  14517  0nninf  14524  peano4nninf  14526  taupi  14591