Theorem mpbir2and 946

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  7196  nqnq0pi  7507  genpassg  7595  addnqpr  7630  mulnqpr  7646  distrprg  7657  1idpr  7661  ltexpri  7682  recexprlemex  7706  aptipr  7710  cauappcvgprlemladd  7727  ltntri  8156  add20  8503  inelr  8613  recgt0  8879  prodgt0  8881  squeeze0  8933  suprzclex  9426  eluzadd  9632  eluzsub  9633  xrletrid  9882  xrre  9897  xrre3  9899  xleadd1a  9950  elioc2  10013  elico2  10014  elicc2  10015  elfz1eq  10112  fztri3or  10116  fznatpl1  10153  nn0fz0  10196  fzctr  10210  fzo1fzo0n0  10261  fzoaddel  10270  zsupcllemstep  10321  zssinfcl  10324  exbtwnz  10342  flid  10376  flqaddz  10389  flqdiv  10415  modqid  10443  frec2uzf1od  10500  iseqf1olemqk  10601  bcval5  10857  abs2difabs  11275  fzomaxdiflem  11279  icodiamlt  11347  dfabsmax  11384  rexico  11388  mul0inf  11408  xrbdtri  11443  sumeq2  11526  sumsnf  11576  fsum00  11629  prodeq2  11724  prodsnf  11759  bitsfzolem  12121  bitsfzo  12122  bitsmod  12123  bitscmp  12125  gcd0id  12156  gcdneg  12159  nn0seqcvgd  12219  lcmval  12241  lcmneg  12252  qredeq  12274  prmind2  12298  pw2dvdseu  12346  hashdvds  12399  pcpremul  12472  pcidlem  12502  pcgcd1  12507  fldivp1  12527  pcfaclem  12528  4sqlem17  12586  ennnfonelemex  12641  ennnfonelemnn0  12649  mnd1  13097  grp1  13248  0subg  13339  nmznsg  13353  ghmpreima  13406  ghmeql  13407  ghmnsgpreima  13409  kerf1ghm  13414  ring1  13625  dvdsrmuld  13662  1unit  13673  unitmulcl  13679  unitgrp  13682  unitnegcl  13696  rhmdvdsr  13741  elrhmunit  13743  subrngintm  13778  subrguss  13802  subrgunit  13805  rhmeql  13816  rhmima  13817  lsslsp  13995  rnglidlrng  14064  fczpsrbag  14235  tgcl  14310  distop  14331  epttop  14336  neiss  14396  opnneissb  14401  ssnei2  14403  innei  14409  lmconst  14462  cnpnei  14465  cnptopco  14468  cnss1  14472  cnss2  14473  cncnpi  14474  cncnp  14476  cnconst2  14479  cnrest  14481  cnptopresti  14484  cnpdis  14488  lmtopcnp  14496  neitx  14514  tx1cn  14515  tx2cn  14516  txcnp  14517  txcnmpt  14519  txdis1cn  14524  psmetsym  14575  psmetres2  14579  isxmetd  14593  xmetsym  14614  xmetpsmet  14615  metrtri  14623  xblss2ps  14650  xblss2  14651  xblcntrps  14659  xblcntr  14660  bdxmet  14747  bdmet  14748  bdmopn  14750  xmetxp  14753  xmetxpbl  14754  rescncf  14827  cncfco  14837  mulcncflem  14853  mulcncf  14854  suplociccreex  14870  ivthinclemlopn  14882  ivthinclemuopn  14884  hovera  14893  hoverlt1  14895  cnplimcim  14913  cnplimclemr  14915  limccnpcntop  14921  limccnp2cntop  14923  limccoap  14924  dvidlemap  14937  dvidrelem  14938  dvidsslem  14939  dvcn  14946  dvaddxxbr  14947  dvmulxxbr  14948  dvcoapbr  14953  dvcjbr  14954  dvrecap  14959  rpabscxpbnd  15186  dvdsppwf1o  15235  lgsdirprm  15285  lgseisenlem1  15321  lgseisenlem2  15322  lgseisenlem3  15323  lgsquadlem1  15328  2sqlem8  15374  refeq  15682  apdifflemf  15700  ltlenmkv  15724