Theorem mpbir2and 896

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 302	. 2 |- ( ph -> ( ch /\ th ) )
4		mpbir2and.3	. 2 |- ( ph -> ( ps <-> ( ch /\ th ) ) )
5	3, 4	mpbird 166	1 |- ( ph -> ps )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nqnq0pi  7147  genpassg  7235  addnqpr  7270  mulnqpr  7286  distrprg  7297  1idpr  7301  ltexpri  7322  recexprlemex  7346  aptipr  7350  cauappcvgprlemladd  7367  ltntri  7761  add20  8103  inelr  8212  recgt0  8466  prodgt0  8468  squeeze0  8520  suprzclex  9001  eluzadd  9204  eluzsub  9205  xrre  9444  xrre3  9446  xleadd1a  9497  elioc2  9560  elico2  9561  elicc2  9562  elfz1eq  9656  fztri3or  9660  fznatpl1  9697  nn0fz0  9740  fzctr  9751  fzo1fzo0n0  9801  fzoaddel  9810  exbtwnz  9869  flid  9898  flqaddz  9911  flqdiv  9935  modqid  9963  frec2uzf1od  10020  iseqf1olemqk  10108  bcval5  10350  abs2difabs  10720  fzomaxdiflem  10724  icodiamlt  10792  dfabsmax  10829  rexico  10833  mul0inf  10851  xrbdtri  10884  sumeq2  10967  sumsnf  11017  fsum00  11070  zsupcllemstep  11433  zssinfcl  11436  gcd0id  11462  gcdneg  11465  nn0seqcvgd  11515  lcmval  11537  lcmneg  11548  qredeq  11570  prmind2  11594  pw2dvdseu  11638  hashdvds  11689  ennnfonelemex  11719  ennnfonelemnn0  11727  tgcl  12015  distop  12036  epttop  12041  neiss  12101  opnneissb  12106  ssnei2  12108  innei  12114  lmconst  12166  cnpnei  12169  cnptopco  12172  cnss1  12176  cnss2  12177  cncnpi  12178  cncnp  12180  cnconst2  12183  cnrest  12185  cnptopresti  12188  cnpdis  12192  lmtopcnp  12200  neitx  12218  tx1cn  12219  tx2cn  12220  txcnp  12221  txcnmpt  12223  txdis1cn  12228  psmetsym  12257  psmetres2  12261  isxmetd  12275  xmetsym  12296  xmetpsmet  12297  metrtri  12305  xblss2ps  12332  xblss2  12333  xblcntrps  12341  xblcntr  12342  bdxmet  12429  bdmet  12430  bdmopn  12432  rescncf  12481  cncfco  12491  mulcncflem  12502  mulcncf  12503  cnplimcim  12516  limccnpcntop  12520  dvidlemap  12533  refeq  12807