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  2176  eqssi  3254  elini  3403  dtruarb  4304  opnzi  4351  so0  4447  we0  4482  ord0  4512  ordon  4608  onsucelsucexmidlem1  4650  regexmidlemm  4654  ordpwsucexmid  4692  reg3exmidlemwe  4701  ordom  4729  funi  5384  funcnvsn  5401  funinsn  5405  fnresi  5476  fn0  5478  f0  5558  fconst  5563  f10  5649  f1o0  5653  f1oi  5654  f1osn  5656  funopsn  5860  isoid  5983  iso0  5990  acexmidlem2  6047  fo1st  6351  fo2nd  6352  iordsmo  6528  tfrlem7  6548  tfrexlem  6565  mapsnf1o2  6931  1domsn  7068  inresflem  7351  0ct  7398  infnninf  7415  infnninfOLD  7416  exmidonfinlem  7496  exmidaclem  7515  pw1on  7536  sucpw1nel3  7543  1pi  7630  prarloclemcalc  7817  ltsopr  7911  ltsosr  8079  cnm  8147  axicn  8178  axaddf  8183  axmulf  8184  nnindnn  8208  mpomulf  8264  ltso  8351  negiso  9229  nnind  9253  0z  9588  dfuzi  9688  cnref1o  9983  elrpii  9989  xrltso  10129  0e0icopnf  10312  0e0iccpnf  10313  fz0to4untppr  10458  fldiv4p1lem1div2  10665  expcl2lemap  10913  expclzaplem  10925  expge0  10937  expge1  10938  xrnegiso  11947  fclim  11979  eff2  12366  reeff1  12386  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  egt2lt3  12466  halfleoddlt  12580  2prm  12824  3prm  12825  1arith  13065  ballotfilemonn  13140  ballotfilem2  13142  setsslnid  13264  xpsff1o  13562  isabli  14017  rngmgpf  14081  mgpf  14155  zringnzr  14750  fntopon  14889  istpsi  14904  ismeti  15211  cnfldms  15401  tgqioo  15420  addcncntoplem  15426  divcnap  15430  abscncf  15450  recncf  15451  imcncf  15452  cjcncf  15453  maxcncf  15480  mincncf  15481  dveflem  15591  reeff1o  15638  reefiso  15642  ioocosf1o  15719  lgslem2  15874  lgsfcl2  15879  lgsne0  15911  2lgslem1b  15962  umgrbien  16105  konigsberglem1  16483  konigsberglem4  16486  ex-fl  16493  bj-indint  16701  bj-omord  16730  012of  16767  2o01f  16768  0nninf  16782  peano4nninf  16784  taupi  16859