Theorem mpbir2and 952

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  3779  nnnninfeq2  7328  nqnq0pi  7658  genpassg  7746  addnqpr  7781  mulnqpr  7797  distrprg  7808  1idpr  7812  ltexpri  7833  recexprlemex  7857  aptipr  7861  cauappcvgprlemladd  7878  ltntri  8307  add20  8654  inelr  8764  recgt0  9030  prodgt0  9032  squeeze0  9084  suprzclex  9578  eluzadd  9785  eluzsub  9786  xrletrid  10040  xrre  10055  xrre3  10057  xleadd1a  10108  elioc2  10171  elico2  10172  elicc2  10173  elfz1eq  10270  fztri3or  10274  fznatpl1  10311  nn0fz0  10354  fzctr  10368  fzo1fzo0n0  10423  fzoaddel  10433  elincfzoext  10439  zsupcllemstep  10490  zssinfcl  10493  exbtwnz  10511  flid  10545  flqaddz  10558  flqdiv  10584  modqid  10612  frec2uzf1od  10669  iseqf1olemqk  10770  bcval5  11026  eqs1  11209  pfxccatin12d  11330  abs2difabs  11673  fzomaxdiflem  11677  icodiamlt  11745  dfabsmax  11782  rexico  11786  mul0inf  11806  xrbdtri  11841  sumeq2  11924  sumsnf  11975  fsum00  12028  prodeq2  12123  prodsnf  12158  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitscmp  12524  gcd0id  12555  gcdneg  12558  nn0seqcvgd  12618  lcmval  12640  lcmneg  12651  qredeq  12673  prmind2  12697  pw2dvdseu  12745  hashdvds  12798  pcpremul  12871  pcidlem  12901  pcgcd1  12906  fldivp1  12926  pcfaclem  12927  4sqlem17  12985  ennnfonelemex  13040  ennnfonelemnn0  13048  mnd1  13543  grp1  13694  0subg  13791  nmznsg  13805  ghmpreima  13858  ghmeql  13859  ghmnsgpreima  13861  kerf1ghm  13866  ring1  14078  dvdsrmuld  14116  1unit  14127  unitmulcl  14133  unitgrp  14136  unitnegcl  14150  rhmdvdsr  14195  elrhmunit  14197  subrngintm  14232  subrguss  14256  subrgunit  14259  rhmeql  14270  rhmima  14271  lsslsp  14449  rnglidlrng  14518  fczpsrbag  14691  mplsubgfilemm  14718  mplsubgfilemcl  14719  mplsubgfileminv  14720  tgcl  14794  distop  14815  epttop  14820  neiss  14880  opnneissb  14885  ssnei2  14887  innei  14893  lmconst  14946  cnpnei  14949  cnptopco  14952  cnss1  14956  cnss2  14957  cncnpi  14958  cncnp  14960  cnconst2  14963  cnrest  14965  cnptopresti  14968  cnpdis  14972  lmtopcnp  14980  neitx  14998  tx1cn  14999  tx2cn  15000  txcnp  15001  txcnmpt  15003  txdis1cn  15008  psmetsym  15059  psmetres2  15063  isxmetd  15077  xmetsym  15098  xmetpsmet  15099  metrtri  15107  xblss2ps  15134  xblss2  15135  xblcntrps  15143  xblcntr  15144  bdxmet  15231  bdmet  15232  bdmopn  15234  xmetxp  15237  xmetxpbl  15238  rescncf  15311  cncfco  15321  mulcncflem  15337  mulcncf  15338  suplociccreex  15354  ivthinclemlopn  15366  ivthinclemuopn  15368  hovera  15377  hoverlt1  15379  cnplimcim  15397  cnplimclemr  15399  limccnpcntop  15405  limccnp2cntop  15407  limccoap  15408  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvcn  15430  dvaddxxbr  15431  dvmulxxbr  15432  dvcoapbr  15437  dvcjbr  15438  dvrecap  15443  rpabscxpbnd  15670  dvdsppwf1o  15719  lgsdirprm  15769  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgsquadlem1  15812  2sqlem8  15858  uspgr2wlkeq2  16223  clwwlknccat  16280  clwwlknonex2lem2  16295  eupthres  16314  refeq  16658  apdifflemf  16676  ltlenmkv  16700