Theorem mpbir2and 885

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypotheses

Ref	Expression
mpbir2and.1	|- ( ph -> ch )
mpbir2and.2	|- ( ph -> th )
mpbir2and.3	|- ( ph -> ( ps <-> ( ch /\ th ) ) )

Assertion

Ref	Expression
mpbir2and	|- ( ph -> ps )

Proof of Theorem mpbir2and

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 |- ( ph -> ch )
2		mpbir2and.2	. . 3 |- ( ph -> th )
3	1, 2	jca 300	. 2 |- ( ph -> ( ch /\ th ) )
4		mpbir2and.3	. 2 |- ( ph -> ( ps <-> ( ch /\ th ) ) )
5	3, 4	mpbird 165	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nqnq0pi  6628  genpassg  6716  addnqpr  6751  mulnqpr  6767  distrprg  6778  1idpr  6782  ltexpri  6803  recexprlemex  6827  aptipr  6831  cauappcvgprlemladd  6848  add20  7578  inelr  7684  recgt0  7928  prodgt0  7930  squeeze0  7982  suprzclex  8445  eluzadd  8647  eluzsub  8648  xrre  8887  xrre3  8889  elioc2  8959  elico2  8960  elicc2  8961  elfz1eq  9054  fztri3or  9058  fznatpl1  9093  nn0fz0  9133  fzctr  9144  fzo1fzo0n0  9192  fzoaddel  9201  qbtwnz  9260  flid  9286  flqaddz  9299  flqdiv  9323  modqid  9351  frec2uzf1od  9408  expival  9478  ibcval5  9690  abs2difabs  9994  fzomaxdiflem  9998  icodiamlt  10066  dfabsmax  10103  rexico  10107  zsupcllemstep  10341  zssinfcl  10344  gcd0id  10370  gcdneg  10373  nn0seqcvgd  10423  lcmval  10445  lcmneg  10456  qredeq  10478  prmind2  10502  pw2dvdseu  10546