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

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  1206  euequ1  2182  eqssi  3264  elini  3413  dtruarb  4323  opnzi  4370  so0  4466  we0  4501  ord0  4531  ordon  4628  onsucelsucexmidlem1  4670  regexmidlemm  4674  ordpwsucexmid  4712  reg3exmidlemwe  4721  ordom  4749  funi  5404  funcnvsn  5421  funinsn  5425  fnresi  5496  fn0  5498  f0  5578  fconst  5583  f10  5669  f1o0  5673  f1oi  5674  f1osn  5676  funopsn  5882  isoid  6006  iso0  6013  rinvf1o  6025  acexmidlem2  6072  fo1st  6381  fo2nd  6382  iordsmo  6558  tfrlem7  6578  tfrexlem  6595  mapsnf1o2  6968  1domsn  7105  inresflem  7390  0ct  7437  infnninf  7454  infnninfOLD  7455  exmidonfinlem  7535  exmidaclem  7554  pw1on  7575  sucpw1nel3  7582  1pi  7672  prarloclemcalc  7859  ltsopr  7953  ltsosr  8121  cnm  8189  axicn  8220  axaddf  8225  axmulf  8226  nnindnn  8250  mpomulf  8306  ltso  8393  negiso  9275  nnind  9299  0z  9634  dfuzi  9735  cnref1o  10030  elrpii  10036  xrltso  10177  0e0icopnf  10360  0e0iccpnf  10361  fz0to4untppr  10509  fldiv4p1lem1div2  10718  expcl2lemap  10966  expclzaplem  10978  expge0  10990  expge1  10991  xrnegiso  12006  fclim  12038  eff2  12425  reeff1  12445  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  egt2lt3  12525  halfleoddlt  12639  2prm  12883  3prm  12884  1arith  13124  ballotfilemonn  13199  ballotfilem2  13206  setsslnid  13382  xpsff1o  13647  isabli  14080  rngmgpf  14211  mgpf  14289  zringnzr  14909  fntopon  15048  istpsi  15063  ismeti  15370  cnfldms  15560  tgqioo  15579  addcncntoplem  15585  divcnap  15589  abscncf  15609  recncf  15610  imcncf  15611  cjcncf  15612  maxcncf  15639  mincncf  15640  dveflem  15750  reeff1o  15797  reefiso  15801  ioocosf1o  15878  lgslem2  16034  lgsfcl2  16039  lgsne0  16071  2lgslem1b  16122  umgrbien  16265  konigsberglem1  16643  konigsberglem4  16646  ex-fl  16653  bj-indint  16871  bj-omord  16900  012of  16937  2o01f  16938  0nninf  16952  peano4nninf  16954  taupi  17028