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  7129  nqnq0pi  7439  genpassg  7527  addnqpr  7562  mulnqpr  7578  distrprg  7589  1idpr  7593  ltexpri  7614  recexprlemex  7638  aptipr  7642  cauappcvgprlemladd  7659  ltntri  8087  add20  8433  inelr  8543  recgt0  8809  prodgt0  8811  squeeze0  8863  suprzclex  9353  eluzadd  9558  eluzsub  9559  xrletrid  9807  xrre  9822  xrre3  9824  xleadd1a  9875  elioc2  9938  elico2  9939  elicc2  9940  elfz1eq  10037  fztri3or  10041  fznatpl1  10078  nn0fz0  10121  fzctr  10135  fzo1fzo0n0  10185  fzoaddel  10194  exbtwnz  10253  flid  10286  flqaddz  10299  flqdiv  10323  modqid  10351  frec2uzf1od  10408  iseqf1olemqk  10496  bcval5  10745  abs2difabs  11119  fzomaxdiflem  11123  icodiamlt  11191  dfabsmax  11228  rexico  11232  mul0inf  11251  xrbdtri  11286  sumeq2  11369  sumsnf  11419  fsum00  11472  prodeq2  11567  prodsnf  11602  zsupcllemstep  11948  zssinfcl  11951  gcd0id  11982  gcdneg  11985  nn0seqcvgd  12043  lcmval  12065  lcmneg  12076  qredeq  12098  prmind2  12122  pw2dvdseu  12170  hashdvds  12223  pcpremul  12295  pcidlem  12324  pcgcd1  12329  fldivp1  12348  pcfaclem  12349  ennnfonelemex  12417  ennnfonelemnn0  12425  mnd1  12852  grp1  12981  0subg  13064  nmznsg  13078  ring1  13241  dvdsrmuld  13270  1unit  13281  unitmulcl  13287  unitgrp  13290  unitnegcl  13304  subrguss  13362  subrgunit  13365  tgcl  13603  distop  13624  epttop  13629  neiss  13689  opnneissb  13694  ssnei2  13696  innei  13702  lmconst  13755  cnpnei  13758  cnptopco  13761  cnss1  13765  cnss2  13766  cncnpi  13767  cncnp  13769  cnconst2  13772  cnrest  13774  cnptopresti  13777  cnpdis  13781  lmtopcnp  13789  neitx  13807  tx1cn  13808  tx2cn  13809  txcnp  13810  txcnmpt  13812  txdis1cn  13817  psmetsym  13868  psmetres2  13872  isxmetd  13886  xmetsym  13907  xmetpsmet  13908  metrtri  13916  xblss2ps  13943  xblss2  13944  xblcntrps  13952  xblcntr  13953  bdxmet  14040  bdmet  14041  bdmopn  14043  xmetxp  14046  xmetxpbl  14047  rescncf  14107  cncfco  14117  mulcncflem  14129  mulcncf  14130  suplociccreex  14141  ivthinclemlopn  14153  ivthinclemuopn  14155  cnplimcim  14175  cnplimclemr  14177  limccnpcntop  14183  limccnp2cntop  14185  limccoap  14186  dvidlemap  14199  dvcn  14203  dvaddxxbr  14204  dvmulxxbr  14205  dvcoapbr  14210  dvcjbr  14211  dvrecap  14216  rpabscxpbnd  14398  lgsdirprm  14474  lgseisenlem1  14489  lgseisenlem2  14490  2sqlem8  14509  refeq  14815  apdifflemf  14833  ltlenmkv  14857