Theorem mpbir2and 944

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

Syntax hints:   -> wi 4   /\ 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:  nnnninfeq2  7122  nqnq0pi  7432  genpassg  7520  addnqpr  7555  mulnqpr  7571  distrprg  7582  1idpr  7586  ltexpri  7607  recexprlemex  7631  aptipr  7635  cauappcvgprlemladd  7652  ltntri  8079  add20  8425  inelr  8535  recgt0  8801  prodgt0  8803  squeeze0  8855  suprzclex  9345  eluzadd  9550  eluzsub  9551  xrletrid  9799  xrre  9814  xrre3  9816  xleadd1a  9867  elioc2  9930  elico2  9931  elicc2  9932  elfz1eq  10028  fztri3or  10032  fznatpl1  10069  nn0fz0  10112  fzctr  10126  fzo1fzo0n0  10176  fzoaddel  10185  exbtwnz  10244  flid  10277  flqaddz  10290  flqdiv  10314  modqid  10342  frec2uzf1od  10399  iseqf1olemqk  10487  bcval5  10734  abs2difabs  11108  fzomaxdiflem  11112  icodiamlt  11180  dfabsmax  11217  rexico  11221  mul0inf  11240  xrbdtri  11275  sumeq2  11358  sumsnf  11408  fsum00  11461  prodeq2  11556  prodsnf  11591  zsupcllemstep  11936  zssinfcl  11939  gcd0id  11970  gcdneg  11973  nn0seqcvgd  12031  lcmval  12053  lcmneg  12064  qredeq  12086  prmind2  12110  pw2dvdseu  12158  hashdvds  12211  pcpremul  12283  pcidlem  12312  pcgcd1  12317  fldivp1  12336  pcfaclem  12337  ennnfonelemex  12405  ennnfonelemnn0  12413  mnd1  12775  grp1  12904  0subg  12985  ring1  13136  dvdsrmuld  13164  1unit  13175  unitmulcl  13181  unitgrp  13184  unitnegcl  13198  tgcl  13346  distop  13367  epttop  13372  neiss  13432  opnneissb  13437  ssnei2  13439  innei  13445  lmconst  13498  cnpnei  13501  cnptopco  13504  cnss1  13508  cnss2  13509  cncnpi  13510  cncnp  13512  cnconst2  13515  cnrest  13517  cnptopresti  13520  cnpdis  13524  lmtopcnp  13532  neitx  13550  tx1cn  13551  tx2cn  13552  txcnp  13553  txcnmpt  13555  txdis1cn  13560  psmetsym  13611  psmetres2  13615  isxmetd  13629  xmetsym  13650  xmetpsmet  13651  metrtri  13659  xblss2ps  13686  xblss2  13687  xblcntrps  13695  xblcntr  13696  bdxmet  13783  bdmet  13784  bdmopn  13786  xmetxp  13789  xmetxpbl  13790  rescncf  13850  cncfco  13860  mulcncflem  13872  mulcncf  13873  suplociccreex  13884  ivthinclemlopn  13896  ivthinclemuopn  13898  cnplimcim  13918  cnplimclemr  13920  limccnpcntop  13926  limccnp2cntop  13928  limccoap  13929  dvidlemap  13942  dvcn  13946  dvaddxxbr  13947  dvmulxxbr  13948  dvcoapbr  13953  dvcjbr  13954  dvrecap  13959  rpabscxpbnd  14141  lgsdirprm  14217  2sqlem8  14241  refeq  14547  apdifflemf  14565  ltlenmkv  14588