Theorem mpbir2and 945

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  7140  nqnq0pi  7450  genpassg  7538  addnqpr  7573  mulnqpr  7589  distrprg  7600  1idpr  7604  ltexpri  7625  recexprlemex  7649  aptipr  7653  cauappcvgprlemladd  7670  ltntri  8098  add20  8444  inelr  8554  recgt0  8820  prodgt0  8822  squeeze0  8874  suprzclex  9364  eluzadd  9569  eluzsub  9570  xrletrid  9818  xrre  9833  xrre3  9835  xleadd1a  9886  elioc2  9949  elico2  9950  elicc2  9951  elfz1eq  10048  fztri3or  10052  fznatpl1  10089  nn0fz0  10132  fzctr  10146  fzo1fzo0n0  10196  fzoaddel  10205  exbtwnz  10264  flid  10297  flqaddz  10310  flqdiv  10334  modqid  10362  frec2uzf1od  10419  iseqf1olemqk  10507  bcval5  10756  abs2difabs  11130  fzomaxdiflem  11134  icodiamlt  11202  dfabsmax  11239  rexico  11243  mul0inf  11262  xrbdtri  11297  sumeq2  11380  sumsnf  11430  fsum00  11483  prodeq2  11578  prodsnf  11613  zsupcllemstep  11959  zssinfcl  11962  gcd0id  11993  gcdneg  11996  nn0seqcvgd  12054  lcmval  12076  lcmneg  12087  qredeq  12109  prmind2  12133  pw2dvdseu  12181  hashdvds  12234  pcpremul  12306  pcidlem  12335  pcgcd1  12340  fldivp1  12359  pcfaclem  12360  ennnfonelemex  12428  ennnfonelemnn0  12436  mnd1  12868  grp1  13002  0subg  13090  nmznsg  13104  ring1  13304  dvdsrmuld  13339  1unit  13350  unitmulcl  13356  unitgrp  13359  unitnegcl  13373  subrngintm  13427  subrguss  13451  subrgunit  13454  lsslsp  13613  tgcl  13835  distop  13856  epttop  13861  neiss  13921  opnneissb  13926  ssnei2  13928  innei  13934  lmconst  13987  cnpnei  13990  cnptopco  13993  cnss1  13997  cnss2  13998  cncnpi  13999  cncnp  14001  cnconst2  14004  cnrest  14006  cnptopresti  14009  cnpdis  14013  lmtopcnp  14021  neitx  14039  tx1cn  14040  tx2cn  14041  txcnp  14042  txcnmpt  14044  txdis1cn  14049  psmetsym  14100  psmetres2  14104  isxmetd  14118  xmetsym  14139  xmetpsmet  14140  metrtri  14148  xblss2ps  14175  xblss2  14176  xblcntrps  14184  xblcntr  14185  bdxmet  14272  bdmet  14273  bdmopn  14275  xmetxp  14278  xmetxpbl  14279  rescncf  14339  cncfco  14349  mulcncflem  14361  mulcncf  14362  suplociccreex  14373  ivthinclemlopn  14385  ivthinclemuopn  14387  cnplimcim  14407  cnplimclemr  14409  limccnpcntop  14415  limccnp2cntop  14417  limccoap  14418  dvidlemap  14431  dvcn  14435  dvaddxxbr  14436  dvmulxxbr  14437  dvcoapbr  14442  dvcjbr  14443  dvrecap  14448  rpabscxpbnd  14630  lgsdirprm  14706  lgseisenlem1  14721  lgseisenlem2  14722  2sqlem8  14741  refeq  15048  apdifflemf  15066  ltlenmkv  15090