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  7103  nqnq0pi  7393  genpassg  7481  addnqpr  7516  mulnqpr  7532  distrprg  7543  1idpr  7547  ltexpri  7568  recexprlemex  7592  aptipr  7596  cauappcvgprlemladd  7613  ltntri  8040  add20  8386  inelr  8496  recgt0  8759  prodgt0  8761  squeeze0  8813  suprzclex  9303  eluzadd  9508  eluzsub  9509  xrletrid  9755  xrre  9770  xrre3  9772  xleadd1a  9823  elioc2  9886  elico2  9887  elicc2  9888  elfz1eq  9984  fztri3or  9988  fznatpl1  10025  nn0fz0  10068  fzctr  10082  fzo1fzo0n0  10132  fzoaddel  10141  exbtwnz  10200  flid  10233  flqaddz  10246  flqdiv  10270  modqid  10298  frec2uzf1od  10355  iseqf1olemqk  10443  bcval5  10690  abs2difabs  11065  fzomaxdiflem  11069  icodiamlt  11137  dfabsmax  11174  rexico  11178  mul0inf  11197  xrbdtri  11232  sumeq2  11315  sumsnf  11365  fsum00  11418  prodeq2  11513  prodsnf  11548  zsupcllemstep  11893  zssinfcl  11896  gcd0id  11927  gcdneg  11930  nn0seqcvgd  11988  lcmval  12010  lcmneg  12021  qredeq  12043  prmind2  12067  pw2dvdseu  12115  hashdvds  12168  pcpremul  12240  pcidlem  12269  pcgcd1  12274  fldivp1  12293  pcfaclem  12294  ennnfonelemex  12362  ennnfonelemnn0  12370  mnd1  12672  tgcl  12823  distop  12844  epttop  12849  neiss  12909  opnneissb  12914  ssnei2  12916  innei  12922  lmconst  12975  cnpnei  12978  cnptopco  12981  cnss1  12985  cnss2  12986  cncnpi  12987  cncnp  12989  cnconst2  12992  cnrest  12994  cnptopresti  12997  cnpdis  13001  lmtopcnp  13009  neitx  13027  tx1cn  13028  tx2cn  13029  txcnp  13030  txcnmpt  13032  txdis1cn  13037  psmetsym  13088  psmetres2  13092  isxmetd  13106  xmetsym  13127  xmetpsmet  13128  metrtri  13136  xblss2ps  13163  xblss2  13164  xblcntrps  13172  xblcntr  13173  bdxmet  13260  bdmet  13261  bdmopn  13263  xmetxp  13266  xmetxpbl  13267  rescncf  13327  cncfco  13337  mulcncflem  13349  mulcncf  13350  suplociccreex  13361  ivthinclemlopn  13373  ivthinclemuopn  13375  cnplimcim  13395  cnplimclemr  13397  limccnpcntop  13403  limccnp2cntop  13405  limccoap  13406  dvidlemap  13419  dvcn  13423  dvaddxxbr  13424  dvmulxxbr  13425  dvcoapbr  13430  dvcjbr  13431  dvrecap  13436  rpabscxpbnd  13618  lgsdirprm  13694  2sqlem8  13718  refeq  14025  apdifflemf  14043