Theorem mpbir2and 957

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpprsnssdc  3820  isfsuppfid  7297  nnnninfeq2  7476  nqnq0pi  7812  genpassg  7900  addnqpr  7935  mulnqpr  7951  distrprg  7962  1idpr  7966  ltexpri  7987  recexprlemex  8011  aptipr  8015  cauappcvgprlemladd  8032  letrid  8450  ltntri  8462  add20  8810  inelr  8921  recgt0  9189  prodgt0  9191  squeeze0  9243  suprzclex  9755  eluzadd  9967  eluzsub  9968  xrletrid  10224  xrre  10239  xrre3  10241  xleadd1a  10292  elioc2  10355  elico2  10356  elicc2  10357  elfz1eq  10456  fztri3or  10460  fzspl  10493  fznatpl1  10500  nn0fz0  10543  fzctr  10557  fzo1fzo0n0  10612  fzoaddel  10622  elincfzoext  10628  zsupcllemstep  10679  zssinfcl  10682  exbtwnz  10702  flid  10740  flqaddz  10753  flqdiv  10779  modqid  10807  frec2uzf1od  10864  iseqf1olemqk  10965  bcval5  11223  hashf1lem1  11307  eqs1  11418  pfxccatin12d  11539  abs2difabs  11897  fzomaxdiflem  11901  icodiamlt  11969  dfabsmax  12006  rexico  12010  mul0inf  12032  xrbdtri  12067  sumeq2  12150  sumsnf  12201  fsum00  12254  prodeq2  12349  prodsnf  12384  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitscmp  12750  gcd0id  12781  gcdneg  12784  nn0seqcvgd  12844  lcmval  12866  lcmneg  12877  qredeq  12899  prmind2  12923  pcpremul  13101  pcidlem  13131  pcgcd1  13136  fldivp1  13156  pcfaclem  13157  4sqlem17  13215  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemex  13363  ennnfonelemnn0  13371  mnd1  13821  grp1  13970  0subg  14061  nmznsg  14075  ghmpreima  14128  ghmeql  14129  ghmnsgpreima  14131  kerf1ghm  14136  cntzsgrpcl  14167  cntzsubm  14170  cntzsubg  14171  cntzmhm  14173  ring1  14471  dvdsrmuld  14512  1unit  14523  unitmulcl  14529  unitgrp  14532  unitnegcl  14546  rhmdvdsr  14591  elrhmunit  14593  subrngintm  14629  subrguss  14653  subrgunit  14656  rhmeql  14667  rhmima  14668  lsslsp  14875  rnglidlrng  14944  issubassa  15122  issubassa2  15144  fczpsrbag  15170  psrbaglecl  15173  psrbagcon  15174  tgcl  15323  distop  15344  epttop  15349  neiss  15409  opnneissb  15414  ssnei2  15416  innei  15422  lmconst  15475  cnpnei  15478  cnptopco  15481  cnss1  15485  cnss2  15486  cncnpi  15487  cncnp  15489  cnconst2  15492  cnrest  15494  cnptopresti  15497  cnpdis  15501  lmtopcnp  15509  neitx  15527  tx1cn  15528  tx2cn  15529  txcnp  15530  txcnmpt  15532  txdis1cn  15537  psmetsym  15588  psmetres2  15592  isxmetd  15606  xmetsym  15627  xmetpsmet  15628  metrtri  15636  xblss2ps  15663  xblss2  15664  xblcntrps  15672  xblcntr  15673  bdxmet  15760  bdmet  15761  bdmopn  15763  xmetxp  15766  xmetxpbl  15767  rescncf  15840  cncfco  15850  mulcncflem  15866  mulcncf  15867  suplociccreex  15883  ivthinclemlopn  15895  ivthinclemuopn  15897  hovera  15906  hoverlt1  15908  cnplimcim  15926  cnplimclemr  15928  limccnpcntop  15934  limccnp2cntop  15936  limccoap  15937  dvidlemap  15950  dvidrelem  15951  dvidsslem  15952  dvcn  15959  dvaddxxbr  15960  dvmulxxbr  15961  dvcoapbr  15966  dvcjbr  15967  dvrecap  15972  rpabscxpbnd  16208  dvdsppwf1o  16316  chtqub  16329  bposlem1  16344  bposlem2  16345  lgsdirprm  16391  lgseisenlem1  16427  lgseisenlem2  16428  lgseisenlem3  16429  lgsquadlem1  16434  2sqlem8  16480  uspgr2wlkeq2  16845  clwwlknccat  16902  clwwlknonex2lem2  16917  eupthres  16936  refeq  17312  apdifflemf  17335  ltlenmkv  17360