Theorem mpbir2and 953

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:  ifpprsnssdc  3798  isfsuppd  7242  nnnninfeq2  7419  nqnq0pi  7752  genpassg  7840  addnqpr  7875  mulnqpr  7891  distrprg  7902  1idpr  7906  ltexpri  7927  recexprlemex  7951  aptipr  7955  cauappcvgprlemladd  7972  ltntri  8400  add20  8747  inelr  8857  recgt0  9123  prodgt0  9125  squeeze0  9177  suprzclex  9675  eluzadd  9882  eluzsub  9883  xrletrid  10137  xrre  10152  xrre3  10154  xleadd1a  10205  elioc2  10268  elico2  10269  elicc2  10270  elfz1eq  10368  fztri3or  10372  fznatpl1  10409  nn0fz0  10452  fzctr  10466  fzo1fzo0n0  10521  fzoaddel  10531  elincfzoext  10537  zsupcllemstep  10588  zssinfcl  10591  exbtwnz  10609  flid  10643  flqaddz  10656  flqdiv  10682  modqid  10710  frec2uzf1od  10767  iseqf1olemqk  10868  bcval5  11124  eqs1  11312  pfxccatin12d  11433  abs2difabs  11789  fzomaxdiflem  11793  icodiamlt  11861  dfabsmax  11898  rexico  11902  mul0inf  11922  xrbdtri  11957  sumeq2  12040  sumsnf  12091  fsum00  12144  prodeq2  12239  prodsnf  12274  bitsfzolem  12636  bitsfzo  12637  bitsmod  12638  bitscmp  12640  gcd0id  12671  gcdneg  12674  nn0seqcvgd  12734  lcmval  12756  lcmneg  12767  qredeq  12789  prmind2  12813  pw2dvdseu  12861  pcpremul  12987  pcidlem  13017  pcgcd1  13022  fldivp1  13042  pcfaclem  13043  4sqlem17  13101  ennnfonelemex  13157  ennnfonelemnn0  13165  mnd1  13660  grp1  13811  0subg  13908  nmznsg  13922  ghmpreima  13975  ghmeql  13976  ghmnsgpreima  13978  kerf1ghm  13983  ring1  14195  dvdsrmuld  14233  1unit  14244  unitmulcl  14250  unitgrp  14253  unitnegcl  14267  rhmdvdsr  14312  elrhmunit  14314  subrngintm  14349  subrguss  14373  subrgunit  14376  rhmeql  14387  rhmima  14388  lsslsp  14569  rnglidlrng  14638  fczpsrbag  14812  psrbaglecl  14816  psrbagcon  14818  mplsubgfilemm  14845  mplsubgfilemcl  14846  mplsubgfileminv  14847  tgcl  14921  distop  14942  epttop  14947  neiss  15007  opnneissb  15012  ssnei2  15014  innei  15020  lmconst  15073  cnpnei  15076  cnptopco  15079  cnss1  15083  cnss2  15084  cncnpi  15085  cncnp  15087  cnconst2  15090  cnrest  15092  cnptopresti  15095  cnpdis  15099  lmtopcnp  15107  neitx  15125  tx1cn  15126  tx2cn  15127  txcnp  15128  txcnmpt  15130  txdis1cn  15135  psmetsym  15186  psmetres2  15190  isxmetd  15204  xmetsym  15225  xmetpsmet  15226  metrtri  15234  xblss2ps  15261  xblss2  15262  xblcntrps  15270  xblcntr  15271  bdxmet  15358  bdmet  15359  bdmopn  15361  xmetxp  15364  xmetxpbl  15365  rescncf  15438  cncfco  15448  mulcncflem  15464  mulcncf  15465  suplociccreex  15481  ivthinclemlopn  15493  ivthinclemuopn  15495  hovera  15504  hoverlt1  15506  cnplimcim  15524  cnplimclemr  15526  limccnpcntop  15532  limccnp2cntop  15534  limccoap  15535  dvidlemap  15548  dvidrelem  15549  dvidsslem  15550  dvcn  15557  dvaddxxbr  15558  dvmulxxbr  15559  dvcoapbr  15564  dvcjbr  15565  dvrecap  15570  rpabscxpbnd  15797  dvdsppwf1o  15849  lgsdirprm  15899  lgseisenlem1  15935  lgseisenlem2  15936  lgseisenlem3  15937  lgsquadlem1  15942  2sqlem8  15988  uspgr2wlkeq2  16353  clwwlknccat  16410  clwwlknonex2lem2  16425  eupthres  16444  refeq  16800  apdifflemf  16822  ltlenmkv  16847