Theorem mpbir2and 953

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:  ifpprsnssdc  3783  nnnninfeq2  7371  nqnq0pi  7701  genpassg  7789  addnqpr  7824  mulnqpr  7840  distrprg  7851  1idpr  7855  ltexpri  7876  recexprlemex  7900  aptipr  7904  cauappcvgprlemladd  7921  ltntri  8350  add20  8697  inelr  8807  recgt0  9073  prodgt0  9075  squeeze0  9127  suprzclex  9621  eluzadd  9828  eluzsub  9829  xrletrid  10083  xrre  10098  xrre3  10100  xleadd1a  10151  elioc2  10214  elico2  10215  elicc2  10216  elfz1eq  10313  fztri3or  10317  fznatpl1  10354  nn0fz0  10397  fzctr  10411  fzo1fzo0n0  10466  fzoaddel  10476  elincfzoext  10482  zsupcllemstep  10533  zssinfcl  10536  exbtwnz  10554  flid  10588  flqaddz  10601  flqdiv  10627  modqid  10655  frec2uzf1od  10712  iseqf1olemqk  10813  bcval5  11069  eqs1  11252  pfxccatin12d  11373  abs2difabs  11729  fzomaxdiflem  11733  icodiamlt  11801  dfabsmax  11838  rexico  11842  mul0inf  11862  xrbdtri  11897  sumeq2  11980  sumsnf  12031  fsum00  12084  prodeq2  12179  prodsnf  12214  bitsfzolem  12576  bitsfzo  12577  bitsmod  12578  bitscmp  12580  gcd0id  12611  gcdneg  12614  nn0seqcvgd  12674  lcmval  12696  lcmneg  12707  qredeq  12729  prmind2  12753  pw2dvdseu  12801  hashdvds  12854  pcpremul  12927  pcidlem  12957  pcgcd1  12962  fldivp1  12982  pcfaclem  12983  4sqlem17  13041  ennnfonelemex  13096  ennnfonelemnn0  13104  mnd1  13599  grp1  13750  0subg  13847  nmznsg  13861  ghmpreima  13914  ghmeql  13915  ghmnsgpreima  13917  kerf1ghm  13922  ring1  14134  dvdsrmuld  14172  1unit  14183  unitmulcl  14189  unitgrp  14192  unitnegcl  14206  rhmdvdsr  14251  elrhmunit  14253  subrngintm  14288  subrguss  14312  subrgunit  14315  rhmeql  14326  rhmima  14327  lsslsp  14505  rnglidlrng  14574  fczpsrbag  14747  psrbaglecl  14751  psrbagcon  14752  mplsubgfilemm  14779  mplsubgfilemcl  14780  mplsubgfileminv  14781  tgcl  14855  distop  14876  epttop  14881  neiss  14941  opnneissb  14946  ssnei2  14948  innei  14954  lmconst  15007  cnpnei  15010  cnptopco  15013  cnss1  15017  cnss2  15018  cncnpi  15019  cncnp  15021  cnconst2  15024  cnrest  15026  cnptopresti  15029  cnpdis  15033  lmtopcnp  15041  neitx  15059  tx1cn  15060  tx2cn  15061  txcnp  15062  txcnmpt  15064  txdis1cn  15069  psmetsym  15120  psmetres2  15124  isxmetd  15138  xmetsym  15159  xmetpsmet  15160  metrtri  15168  xblss2ps  15195  xblss2  15196  xblcntrps  15204  xblcntr  15205  bdxmet  15292  bdmet  15293  bdmopn  15295  xmetxp  15298  xmetxpbl  15299  rescncf  15372  cncfco  15382  mulcncflem  15398  mulcncf  15399  suplociccreex  15415  ivthinclemlopn  15427  ivthinclemuopn  15429  hovera  15438  hoverlt1  15440  cnplimcim  15458  cnplimclemr  15460  limccnpcntop  15466  limccnp2cntop  15468  limccoap  15469  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvcn  15491  dvaddxxbr  15492  dvmulxxbr  15493  dvcoapbr  15498  dvcjbr  15499  dvrecap  15504  rpabscxpbnd  15731  dvdsppwf1o  15783  lgsdirprm  15833  lgseisenlem1  15869  lgseisenlem2  15870  lgseisenlem3  15871  lgsquadlem1  15876  2sqlem8  15922  uspgr2wlkeq2  16287  clwwlknccat  16344  clwwlknonex2lem2  16359  eupthres  16378  refeq  16736  apdifflemf  16758  ltlenmkv  16783