Theorem mpbir2and 934

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  7089  nqnq0pi  7375  genpassg  7463  addnqpr  7498  mulnqpr  7514  distrprg  7525  1idpr  7529  ltexpri  7550  recexprlemex  7574  aptipr  7578  cauappcvgprlemladd  7595  ltntri  8022  add20  8368  inelr  8478  recgt0  8741  prodgt0  8743  squeeze0  8795  suprzclex  9285  eluzadd  9490  eluzsub  9491  xrletrid  9737  xrre  9752  xrre3  9754  xleadd1a  9805  elioc2  9868  elico2  9869  elicc2  9870  elfz1eq  9966  fztri3or  9970  fznatpl1  10007  nn0fz0  10050  fzctr  10064  fzo1fzo0n0  10114  fzoaddel  10123  exbtwnz  10182  flid  10215  flqaddz  10228  flqdiv  10252  modqid  10280  frec2uzf1od  10337  iseqf1olemqk  10425  bcval5  10672  abs2difabs  11046  fzomaxdiflem  11050  icodiamlt  11118  dfabsmax  11155  rexico  11159  mul0inf  11178  xrbdtri  11213  sumeq2  11296  sumsnf  11346  fsum00  11399  prodeq2  11494  prodsnf  11529  zsupcllemstep  11874  zssinfcl  11877  gcd0id  11908  gcdneg  11911  nn0seqcvgd  11969  lcmval  11991  lcmneg  12002  qredeq  12024  prmind2  12048  pw2dvdseu  12096  hashdvds  12149  pcpremul  12221  pcidlem  12250  pcgcd1  12255  fldivp1  12274  pcfaclem  12275  ennnfonelemex  12343  ennnfonelemnn0  12351  tgcl  12664  distop  12685  epttop  12690  neiss  12750  opnneissb  12755  ssnei2  12757  innei  12763  lmconst  12816  cnpnei  12819  cnptopco  12822  cnss1  12826  cnss2  12827  cncnpi  12828  cncnp  12830  cnconst2  12833  cnrest  12835  cnptopresti  12838  cnpdis  12842  lmtopcnp  12850  neitx  12868  tx1cn  12869  tx2cn  12870  txcnp  12871  txcnmpt  12873  txdis1cn  12878  psmetsym  12929  psmetres2  12933  isxmetd  12947  xmetsym  12968  xmetpsmet  12969  metrtri  12977  xblss2ps  13004  xblss2  13005  xblcntrps  13013  xblcntr  13014  bdxmet  13101  bdmet  13102  bdmopn  13104  xmetxp  13107  xmetxpbl  13108  rescncf  13168  cncfco  13178  mulcncflem  13190  mulcncf  13191  suplociccreex  13202  ivthinclemlopn  13214  ivthinclemuopn  13216  cnplimcim  13236  cnplimclemr  13238  limccnpcntop  13244  limccnp2cntop  13246  limccoap  13247  dvidlemap  13260  dvcn  13264  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  rpabscxpbnd  13459  lgsdirprm  13535  2sqlem8  13559  refeq  13867  apdifflemf  13885