Theorem mpbir2and 946

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:  nnnninfeq2  7188  nqnq0pi  7498  genpassg  7586  addnqpr  7621  mulnqpr  7637  distrprg  7648  1idpr  7652  ltexpri  7673  recexprlemex  7697  aptipr  7701  cauappcvgprlemladd  7718  ltntri  8147  add20  8493  inelr  8603  recgt0  8869  prodgt0  8871  squeeze0  8923  suprzclex  9415  eluzadd  9621  eluzsub  9622  xrletrid  9871  xrre  9886  xrre3  9888  xleadd1a  9939  elioc2  10002  elico2  10003  elicc2  10004  elfz1eq  10101  fztri3or  10105  fznatpl1  10142  nn0fz0  10185  fzctr  10199  fzo1fzo0n0  10250  fzoaddel  10259  exbtwnz  10319  flid  10353  flqaddz  10366  flqdiv  10392  modqid  10420  frec2uzf1od  10477  iseqf1olemqk  10578  bcval5  10834  abs2difabs  11252  fzomaxdiflem  11256  icodiamlt  11324  dfabsmax  11361  rexico  11365  mul0inf  11384  xrbdtri  11419  sumeq2  11502  sumsnf  11552  fsum00  11605  prodeq2  11700  prodsnf  11735  zsupcllemstep  12082  zssinfcl  12085  gcd0id  12116  gcdneg  12119  nn0seqcvgd  12179  lcmval  12201  lcmneg  12212  qredeq  12234  prmind2  12258  pw2dvdseu  12306  hashdvds  12359  pcpremul  12431  pcidlem  12461  pcgcd1  12466  fldivp1  12486  pcfaclem  12487  4sqlem17  12545  ennnfonelemex  12571  ennnfonelemnn0  12579  mnd1  13027  grp1  13178  0subg  13269  nmznsg  13283  ghmpreima  13336  ghmeql  13337  ghmnsgpreima  13339  kerf1ghm  13344  ring1  13555  dvdsrmuld  13592  1unit  13603  unitmulcl  13609  unitgrp  13612  unitnegcl  13626  rhmdvdsr  13671  elrhmunit  13673  subrngintm  13708  subrguss  13732  subrgunit  13735  rhmeql  13746  rhmima  13747  lsslsp  13925  rnglidlrng  13994  fczpsrbag  14157  tgcl  14232  distop  14253  epttop  14258  neiss  14318  opnneissb  14323  ssnei2  14325  innei  14331  lmconst  14384  cnpnei  14387  cnptopco  14390  cnss1  14394  cnss2  14395  cncnpi  14396  cncnp  14398  cnconst2  14401  cnrest  14403  cnptopresti  14406  cnpdis  14410  lmtopcnp  14418  neitx  14436  tx1cn  14437  tx2cn  14438  txcnp  14439  txcnmpt  14441  txdis1cn  14446  psmetsym  14497  psmetres2  14501  isxmetd  14515  xmetsym  14536  xmetpsmet  14537  metrtri  14545  xblss2ps  14572  xblss2  14573  xblcntrps  14581  xblcntr  14582  bdxmet  14669  bdmet  14670  bdmopn  14672  xmetxp  14675  xmetxpbl  14676  rescncf  14736  cncfco  14746  mulcncflem  14761  mulcncf  14762  suplociccreex  14778  ivthinclemlopn  14790  ivthinclemuopn  14792  hovera  14801  hoverlt1  14803  cnplimcim  14821  cnplimclemr  14823  limccnpcntop  14829  limccnp2cntop  14831  limccoap  14832  dvidlemap  14845  dvcn  14849  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  rpabscxpbnd  15073  lgsdirprm  15150  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgsquadlem1  15191  2sqlem8  15210  refeq  15518  apdifflemf  15536  ltlenmkv  15560