Theorem mpbir2and 928

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 304	. 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nqnq0pi  7239  genpassg  7327  addnqpr  7362  mulnqpr  7378  distrprg  7389  1idpr  7393  ltexpri  7414  recexprlemex  7438  aptipr  7442  cauappcvgprlemladd  7459  ltntri  7883  add20  8229  inelr  8339  recgt0  8601  prodgt0  8603  squeeze0  8655  suprzclex  9142  eluzadd  9347  eluzsub  9348  xrre  9596  xrre3  9598  xleadd1a  9649  elioc2  9712  elico2  9713  elicc2  9714  elfz1eq  9808  fztri3or  9812  fznatpl1  9849  nn0fz0  9892  fzctr  9903  fzo1fzo0n0  9953  fzoaddel  9962  exbtwnz  10021  flid  10050  flqaddz  10063  flqdiv  10087  modqid  10115  frec2uzf1od  10172  iseqf1olemqk  10260  bcval5  10502  abs2difabs  10873  fzomaxdiflem  10877  icodiamlt  10945  dfabsmax  10982  rexico  10986  mul0inf  11005  xrbdtri  11038  sumeq2  11121  sumsnf  11171  fsum00  11224  prodeq2  11319  zsupcllemstep  11627  zssinfcl  11630  gcd0id  11656  gcdneg  11659  nn0seqcvgd  11711  lcmval  11733  lcmneg  11744  qredeq  11766  prmind2  11790  pw2dvdseu  11835  hashdvds  11886  ennnfonelemex  11916  ennnfonelemnn0  11924  tgcl  12222  distop  12243  epttop  12248  neiss  12308  opnneissb  12313  ssnei2  12315  innei  12321  lmconst  12374  cnpnei  12377  cnptopco  12380  cnss1  12384  cnss2  12385  cncnpi  12386  cncnp  12388  cnconst2  12391  cnrest  12393  cnptopresti  12396  cnpdis  12400  lmtopcnp  12408  neitx  12426  tx1cn  12427  tx2cn  12428  txcnp  12429  txcnmpt  12431  txdis1cn  12436  psmetsym  12487  psmetres2  12491  isxmetd  12505  xmetsym  12526  xmetpsmet  12527  metrtri  12535  xblss2ps  12562  xblss2  12563  xblcntrps  12571  xblcntr  12572  bdxmet  12659  bdmet  12660  bdmopn  12662  xmetxp  12665  xmetxpbl  12666  rescncf  12726  cncfco  12736  mulcncflem  12748  mulcncf  12749  suplociccreex  12760  ivthinclemlopn  12772  ivthinclemuopn  12774  cnplimcim  12794  cnplimclemr  12796  limccnpcntop  12802  limccnp2cntop  12804  limccoap  12805  dvidlemap  12818  dvcn  12822  dvaddxxbr  12823  dvmulxxbr  12824  dvcoapbr  12829  dvcjbr  12830  dvrecap  12835  refeq  13212