Theorem mpbir2and 947

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  7243  nqnq0pi  7564  genpassg  7652  addnqpr  7687  mulnqpr  7703  distrprg  7714  1idpr  7718  ltexpri  7739  recexprlemex  7763  aptipr  7767  cauappcvgprlemladd  7784  ltntri  8213  add20  8560  inelr  8670  recgt0  8936  prodgt0  8938  squeeze0  8990  suprzclex  9484  eluzadd  9690  eluzsub  9691  xrletrid  9940  xrre  9955  xrre3  9957  xleadd1a  10008  elioc2  10071  elico2  10072  elicc2  10073  elfz1eq  10170  fztri3or  10174  fznatpl1  10211  nn0fz0  10254  fzctr  10268  fzo1fzo0n0  10320  fzoaddel  10329  elincfzoext  10335  zsupcllemstep  10385  zssinfcl  10388  exbtwnz  10406  flid  10440  flqaddz  10453  flqdiv  10479  modqid  10507  frec2uzf1od  10564  iseqf1olemqk  10665  bcval5  10921  eqs1  11096  abs2difabs  11469  fzomaxdiflem  11473  icodiamlt  11541  dfabsmax  11578  rexico  11582  mul0inf  11602  xrbdtri  11637  sumeq2  11720  sumsnf  11770  fsum00  11823  prodeq2  11918  prodsnf  11953  bitsfzolem  12315  bitsfzo  12316  bitsmod  12317  bitscmp  12319  gcd0id  12350  gcdneg  12353  nn0seqcvgd  12413  lcmval  12435  lcmneg  12446  qredeq  12468  prmind2  12492  pw2dvdseu  12540  hashdvds  12593  pcpremul  12666  pcidlem  12696  pcgcd1  12701  fldivp1  12721  pcfaclem  12722  4sqlem17  12780  ennnfonelemex  12835  ennnfonelemnn0  12843  mnd1  13337  grp1  13488  0subg  13585  nmznsg  13599  ghmpreima  13652  ghmeql  13653  ghmnsgpreima  13655  kerf1ghm  13660  ring1  13871  dvdsrmuld  13908  1unit  13919  unitmulcl  13925  unitgrp  13928  unitnegcl  13942  rhmdvdsr  13987  elrhmunit  13989  subrngintm  14024  subrguss  14048  subrgunit  14051  rhmeql  14062  rhmima  14063  lsslsp  14241  rnglidlrng  14310  fczpsrbag  14483  mplsubgfilemm  14510  mplsubgfilemcl  14511  mplsubgfileminv  14512  tgcl  14586  distop  14607  epttop  14612  neiss  14672  opnneissb  14677  ssnei2  14679  innei  14685  lmconst  14738  cnpnei  14741  cnptopco  14744  cnss1  14748  cnss2  14749  cncnpi  14750  cncnp  14752  cnconst2  14755  cnrest  14757  cnptopresti  14760  cnpdis  14764  lmtopcnp  14772  neitx  14790  tx1cn  14791  tx2cn  14792  txcnp  14793  txcnmpt  14795  txdis1cn  14800  psmetsym  14851  psmetres2  14855  isxmetd  14869  xmetsym  14890  xmetpsmet  14891  metrtri  14899  xblss2ps  14926  xblss2  14927  xblcntrps  14935  xblcntr  14936  bdxmet  15023  bdmet  15024  bdmopn  15026  xmetxp  15029  xmetxpbl  15030  rescncf  15103  cncfco  15113  mulcncflem  15129  mulcncf  15130  suplociccreex  15146  ivthinclemlopn  15158  ivthinclemuopn  15160  hovera  15169  hoverlt1  15171  cnplimcim  15189  cnplimclemr  15191  limccnpcntop  15197  limccnp2cntop  15199  limccoap  15200  dvidlemap  15213  dvidrelem  15214  dvidsslem  15215  dvcn  15222  dvaddxxbr  15223  dvmulxxbr  15224  dvcoapbr  15229  dvcjbr  15230  dvrecap  15235  rpabscxpbnd  15462  dvdsppwf1o  15511  lgsdirprm  15561  lgseisenlem1  15597  lgseisenlem2  15598  lgseisenlem3  15599  lgsquadlem1  15604  2sqlem8  15650  refeq  16082  apdifflemf  16100  ltlenmkv  16124