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  3804  isfsuppd  7256  nnnninfeq2  7433  nqnq0pi  7769  genpassg  7857  addnqpr  7892  mulnqpr  7908  distrprg  7919  1idpr  7923  ltexpri  7944  recexprlemex  7968  aptipr  7972  cauappcvgprlemladd  7989  letrid  8406  ltntri  8418  add20  8766  inelr  8876  recgt0  9144  prodgt0  9146  squeeze0  9198  suprzclex  9697  eluzadd  9904  eluzsub  9905  xrletrid  10160  xrre  10175  xrre3  10177  xleadd1a  10228  elioc2  10291  elico2  10292  elicc2  10293  elfz1eq  10392  fztri3or  10396  fzspl  10428  fznatpl1  10435  nn0fz0  10478  fzctr  10492  fzo1fzo0n0  10547  fzoaddel  10557  elincfzoext  10563  zsupcllemstep  10614  zssinfcl  10617  exbtwnz  10637  flid  10671  flqaddz  10684  flqdiv  10710  modqid  10738  frec2uzf1od  10795  iseqf1olemqk  10896  bcval5  11153  eqs1  11344  pfxccatin12d  11465  abs2difabs  11822  fzomaxdiflem  11826  icodiamlt  11894  dfabsmax  11931  rexico  11935  mul0inf  11955  xrbdtri  11990  sumeq2  12073  sumsnf  12124  fsum00  12177  prodeq2  12272  prodsnf  12307  bitsfzolem  12669  bitsfzo  12670  bitsmod  12671  bitscmp  12673  gcd0id  12704  gcdneg  12707  nn0seqcvgd  12767  lcmval  12789  lcmneg  12800  qredeq  12822  prmind2  12846  pw2dvdseu  12894  pcpremul  13020  pcidlem  13050  pcgcd1  13055  fldivp1  13075  pcfaclem  13076  4sqlem17  13134  ballotfilemfc0  13180  ballotfilemfcc  13181  ennnfonelemex  13253  ennnfonelemnn0  13261  mnd1  13714  grp1  13865  0subg  13956  nmznsg  13970  ghmpreima  14023  ghmeql  14024  ghmnsgpreima  14026  kerf1ghm  14031  ring1  14306  dvdsrmuld  14345  1unit  14356  unitmulcl  14362  unitgrp  14365  unitnegcl  14379  rhmdvdsr  14424  elrhmunit  14426  subrngintm  14462  subrguss  14486  subrgunit  14489  rhmeql  14500  rhmima  14501  lsslsp  14707  rnglidlrng  14776  fczpsrbag  14950  psrbaglecl  14954  psrbagcon  14956  mplsubgfilemm  14983  mplsubgfilemcl  14984  mplsubgfileminv  14985  tgcl  15059  distop  15080  epttop  15085  neiss  15145  opnneissb  15150  ssnei2  15152  innei  15158  lmconst  15211  cnpnei  15214  cnptopco  15217  cnss1  15221  cnss2  15222  cncnpi  15223  cncnp  15225  cnconst2  15228  cnrest  15230  cnptopresti  15233  cnpdis  15237  lmtopcnp  15245  neitx  15263  tx1cn  15264  tx2cn  15265  txcnp  15266  txcnmpt  15268  txdis1cn  15273  psmetsym  15324  psmetres2  15328  isxmetd  15342  xmetsym  15363  xmetpsmet  15364  metrtri  15372  xblss2ps  15399  xblss2  15400  xblcntrps  15408  xblcntr  15409  bdxmet  15496  bdmet  15497  bdmopn  15499  xmetxp  15502  xmetxpbl  15503  rescncf  15576  cncfco  15586  mulcncflem  15602  mulcncf  15603  suplociccreex  15619  ivthinclemlopn  15631  ivthinclemuopn  15633  hovera  15642  hoverlt1  15644  cnplimcim  15662  cnplimclemr  15664  limccnpcntop  15670  limccnp2cntop  15672  limccoap  15673  dvidlemap  15686  dvidrelem  15687  dvidsslem  15688  dvcn  15695  dvaddxxbr  15696  dvmulxxbr  15697  dvcoapbr  15702  dvcjbr  15703  dvrecap  15708  rpabscxpbnd  15935  dvdsppwf1o  15987  lgsdirprm  16037  lgseisenlem1  16073  lgseisenlem2  16074  lgseisenlem3  16075  lgsquadlem1  16080  2sqlem8  16126  uspgr2wlkeq2  16491  clwwlknccat  16548  clwwlknonex2lem2  16563  eupthres  16582  refeq  16948  apdifflemf  16970  ltlenmkv  16995