Theorem mpbir2and 944

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  7126  nqnq0pi  7436  genpassg  7524  addnqpr  7559  mulnqpr  7575  distrprg  7586  1idpr  7590  ltexpri  7611  recexprlemex  7635  aptipr  7639  cauappcvgprlemladd  7656  ltntri  8084  add20  8430  inelr  8540  recgt0  8806  prodgt0  8808  squeeze0  8860  suprzclex  9350  eluzadd  9555  eluzsub  9556  xrletrid  9804  xrre  9819  xrre3  9821  xleadd1a  9872  elioc2  9935  elico2  9936  elicc2  9937  elfz1eq  10034  fztri3or  10038  fznatpl1  10075  nn0fz0  10118  fzctr  10132  fzo1fzo0n0  10182  fzoaddel  10191  exbtwnz  10250  flid  10283  flqaddz  10296  flqdiv  10320  modqid  10348  frec2uzf1od  10405  iseqf1olemqk  10493  bcval5  10742  abs2difabs  11116  fzomaxdiflem  11120  icodiamlt  11188  dfabsmax  11225  rexico  11229  mul0inf  11248  xrbdtri  11283  sumeq2  11366  sumsnf  11416  fsum00  11469  prodeq2  11564  prodsnf  11599  zsupcllemstep  11945  zssinfcl  11948  gcd0id  11979  gcdneg  11982  nn0seqcvgd  12040  lcmval  12062  lcmneg  12073  qredeq  12095  prmind2  12119  pw2dvdseu  12167  hashdvds  12220  pcpremul  12292  pcidlem  12321  pcgcd1  12326  fldivp1  12345  pcfaclem  12346  ennnfonelemex  12414  ennnfonelemnn0  12422  mnd1  12846  grp1  12975  0subg  13057  nmznsg  13071  ring1  13234  dvdsrmuld  13263  1unit  13274  unitmulcl  13280  unitgrp  13283  unitnegcl  13297  subrguss  13355  subrgunit  13358  tgcl  13534  distop  13555  epttop  13560  neiss  13620  opnneissb  13625  ssnei2  13627  innei  13633  lmconst  13686  cnpnei  13689  cnptopco  13692  cnss1  13696  cnss2  13697  cncnpi  13698  cncnp  13700  cnconst2  13703  cnrest  13705  cnptopresti  13708  cnpdis  13712  lmtopcnp  13720  neitx  13738  tx1cn  13739  tx2cn  13740  txcnp  13741  txcnmpt  13743  txdis1cn  13748  psmetsym  13799  psmetres2  13803  isxmetd  13817  xmetsym  13838  xmetpsmet  13839  metrtri  13847  xblss2ps  13874  xblss2  13875  xblcntrps  13883  xblcntr  13884  bdxmet  13971  bdmet  13972  bdmopn  13974  xmetxp  13977  xmetxpbl  13978  rescncf  14038  cncfco  14048  mulcncflem  14060  mulcncf  14061  suplociccreex  14072  ivthinclemlopn  14084  ivthinclemuopn  14086  cnplimcim  14106  cnplimclemr  14108  limccnpcntop  14114  limccnp2cntop  14116  limccoap  14117  dvidlemap  14130  dvcn  14134  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147  rpabscxpbnd  14329  lgsdirprm  14405  lgseisenlem1  14420  lgseisenlem2  14421  2sqlem8  14440  refeq  14746  apdifflemf  14764  ltlenmkv  14787