Theorem mpbir2and 939

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 304	. 2 |- ( ph -> ( ch /\ th ) )
4		mpbir2and.3	. 2 |- ( ph -> ( ps <-> ( ch /\ th ) ) )
5	3, 4	mpbird 166	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nnnninfeq2  7105  nqnq0pi  7400  genpassg  7488  addnqpr  7523  mulnqpr  7539  distrprg  7550  1idpr  7554  ltexpri  7575  recexprlemex  7599  aptipr  7603  cauappcvgprlemladd  7620  ltntri  8047  add20  8393  inelr  8503  recgt0  8766  prodgt0  8768  squeeze0  8820  suprzclex  9310  eluzadd  9515  eluzsub  9516  xrletrid  9762  xrre  9777  xrre3  9779  xleadd1a  9830  elioc2  9893  elico2  9894  elicc2  9895  elfz1eq  9991  fztri3or  9995  fznatpl1  10032  nn0fz0  10075  fzctr  10089  fzo1fzo0n0  10139  fzoaddel  10148  exbtwnz  10207  flid  10240  flqaddz  10253  flqdiv  10277  modqid  10305  frec2uzf1od  10362  iseqf1olemqk  10450  bcval5  10697  abs2difabs  11072  fzomaxdiflem  11076  icodiamlt  11144  dfabsmax  11181  rexico  11185  mul0inf  11204  xrbdtri  11239  sumeq2  11322  sumsnf  11372  fsum00  11425  prodeq2  11520  prodsnf  11555  zsupcllemstep  11900  zssinfcl  11903  gcd0id  11934  gcdneg  11937  nn0seqcvgd  11995  lcmval  12017  lcmneg  12028  qredeq  12050  prmind2  12074  pw2dvdseu  12122  hashdvds  12175  pcpremul  12247  pcidlem  12276  pcgcd1  12281  fldivp1  12300  pcfaclem  12301  ennnfonelemex  12369  ennnfonelemnn0  12377  mnd1  12679  tgcl  12858  distop  12879  epttop  12884  neiss  12944  opnneissb  12949  ssnei2  12951  innei  12957  lmconst  13010  cnpnei  13013  cnptopco  13016  cnss1  13020  cnss2  13021  cncnpi  13022  cncnp  13024  cnconst2  13027  cnrest  13029  cnptopresti  13032  cnpdis  13036  lmtopcnp  13044  neitx  13062  tx1cn  13063  tx2cn  13064  txcnp  13065  txcnmpt  13067  txdis1cn  13072  psmetsym  13123  psmetres2  13127  isxmetd  13141  xmetsym  13162  xmetpsmet  13163  metrtri  13171  xblss2ps  13198  xblss2  13199  xblcntrps  13207  xblcntr  13208  bdxmet  13295  bdmet  13296  bdmopn  13298  xmetxp  13301  xmetxpbl  13302  rescncf  13362  cncfco  13372  mulcncflem  13384  mulcncf  13385  suplociccreex  13396  ivthinclemlopn  13408  ivthinclemuopn  13410  cnplimcim  13430  cnplimclemr  13432  limccnpcntop  13438  limccnp2cntop  13440  limccoap  13441  dvidlemap  13454  dvcn  13458  dvaddxxbr  13459  dvmulxxbr  13460  dvcoapbr  13465  dvcjbr  13466  dvrecap  13471  rpabscxpbnd  13653  lgsdirprm  13729  2sqlem8  13753  refeq  14060  apdifflemf  14078