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  7190  nqnq0pi  7500  genpassg  7588  addnqpr  7623  mulnqpr  7639  distrprg  7650  1idpr  7654  ltexpri  7675  recexprlemex  7699  aptipr  7703  cauappcvgprlemladd  7720  ltntri  8149  add20  8495  inelr  8605  recgt0  8871  prodgt0  8873  squeeze0  8925  suprzclex  9418  eluzadd  9624  eluzsub  9625  xrletrid  9874  xrre  9889  xrre3  9891  xleadd1a  9942  elioc2  10005  elico2  10006  elicc2  10007  elfz1eq  10104  fztri3or  10108  fznatpl1  10145  nn0fz0  10188  fzctr  10202  fzo1fzo0n0  10253  fzoaddel  10262  exbtwnz  10322  flid  10356  flqaddz  10369  flqdiv  10395  modqid  10423  frec2uzf1od  10480  iseqf1olemqk  10581  bcval5  10837  abs2difabs  11255  fzomaxdiflem  11259  icodiamlt  11327  dfabsmax  11364  rexico  11368  mul0inf  11387  xrbdtri  11422  sumeq2  11505  sumsnf  11555  fsum00  11608  prodeq2  11703  prodsnf  11738  zsupcllemstep  12085  zssinfcl  12088  gcd0id  12119  gcdneg  12122  nn0seqcvgd  12182  lcmval  12204  lcmneg  12215  qredeq  12237  prmind2  12261  pw2dvdseu  12309  hashdvds  12362  pcpremul  12434  pcidlem  12464  pcgcd1  12469  fldivp1  12489  pcfaclem  12490  4sqlem17  12548  ennnfonelemex  12574  ennnfonelemnn0  12582  mnd1  13030  grp1  13181  0subg  13272  nmznsg  13286  ghmpreima  13339  ghmeql  13340  ghmnsgpreima  13342  kerf1ghm  13347  ring1  13558  dvdsrmuld  13595  1unit  13606  unitmulcl  13612  unitgrp  13615  unitnegcl  13629  rhmdvdsr  13674  elrhmunit  13676  subrngintm  13711  subrguss  13735  subrgunit  13738  rhmeql  13749  rhmima  13750  lsslsp  13928  rnglidlrng  13997  fczpsrbag  14168  tgcl  14243  distop  14264  epttop  14269  neiss  14329  opnneissb  14334  ssnei2  14336  innei  14342  lmconst  14395  cnpnei  14398  cnptopco  14401  cnss1  14405  cnss2  14406  cncnpi  14407  cncnp  14409  cnconst2  14412  cnrest  14414  cnptopresti  14417  cnpdis  14421  lmtopcnp  14429  neitx  14447  tx1cn  14448  tx2cn  14449  txcnp  14450  txcnmpt  14452  txdis1cn  14457  psmetsym  14508  psmetres2  14512  isxmetd  14526  xmetsym  14547  xmetpsmet  14548  metrtri  14556  xblss2ps  14583  xblss2  14584  xblcntrps  14592  xblcntr  14593  bdxmet  14680  bdmet  14681  bdmopn  14683  xmetxp  14686  xmetxpbl  14687  rescncf  14760  cncfco  14770  mulcncflem  14786  mulcncf  14787  suplociccreex  14803  ivthinclemlopn  14815  ivthinclemuopn  14817  hovera  14826  hoverlt1  14828  cnplimcim  14846  cnplimclemr  14848  limccnpcntop  14854  limccnp2cntop  14856  limccoap  14857  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcn  14879  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvrecap  14892  rpabscxpbnd  15114  lgsdirprm  15191  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgsquadlem1  15234  2sqlem8  15280  refeq  15588  apdifflemf  15606  ltlenmkv  15630