Theorem mpbir2and 957

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpprsnssdc  3820  isfsuppd  7290  nnnninfeq2  7470  nqnq0pi  7806  genpassg  7894  addnqpr  7929  mulnqpr  7945  distrprg  7956  1idpr  7960  ltexpri  7981  recexprlemex  8005  aptipr  8009  cauappcvgprlemladd  8026  letrid  8444  ltntri  8456  add20  8804  inelr  8915  recgt0  9183  prodgt0  9185  squeeze0  9237  suprzclex  9749  eluzadd  9961  eluzsub  9962  xrletrid  10218  xrre  10233  xrre3  10235  xleadd1a  10286  elioc2  10349  elico2  10350  elicc2  10351  elfz1eq  10450  fztri3or  10454  fzspl  10487  fznatpl1  10494  nn0fz0  10537  fzctr  10551  fzo1fzo0n0  10606  fzoaddel  10616  elincfzoext  10622  zsupcllemstep  10673  zssinfcl  10676  exbtwnz  10696  flid  10733  flqaddz  10746  flqdiv  10772  modqid  10800  frec2uzf1od  10857  iseqf1olemqk  10958  bcval5  11216  hashf1lem1  11300  eqs1  11411  pfxccatin12d  11532  abs2difabs  11890  fzomaxdiflem  11894  icodiamlt  11962  dfabsmax  11999  rexico  12003  mul0inf  12025  xrbdtri  12060  sumeq2  12143  sumsnf  12194  fsum00  12247  prodeq2  12342  prodsnf  12377  bitsfzolem  12739  bitsfzo  12740  bitsmod  12741  bitscmp  12743  gcd0id  12774  gcdneg  12777  nn0seqcvgd  12837  lcmval  12859  lcmneg  12870  qredeq  12892  prmind2  12916  pcpremul  13094  pcidlem  13124  pcgcd1  13129  fldivp1  13149  pcfaclem  13150  4sqlem17  13208  ballotfilemfc0  13283  ballotfilemfcc  13284  ennnfonelemex  13356  ennnfonelemnn0  13364  mnd1  13813  grp1  13962  0subg  14053  nmznsg  14067  ghmpreima  14120  ghmeql  14121  ghmnsgpreima  14123  kerf1ghm  14128  ring1  14415  dvdsrmuld  14454  1unit  14465  unitmulcl  14471  unitgrp  14474  unitnegcl  14488  rhmdvdsr  14533  elrhmunit  14535  subrngintm  14571  subrguss  14595  subrgunit  14598  rhmeql  14609  rhmima  14610  lsslsp  14817  rnglidlrng  14886  issubassa  15064  issubassa2  15086  fczpsrbag  15107  psrbaglecl  15111  psrbagcon  15113  mplsubgfilemm  15141  mplsubgfilemcl  15142  mplsubgfileminv  15143  tgcl  15217  distop  15238  epttop  15243  neiss  15303  opnneissb  15308  ssnei2  15310  innei  15316  lmconst  15369  cnpnei  15372  cnptopco  15375  cnss1  15379  cnss2  15380  cncnpi  15381  cncnp  15383  cnconst2  15386  cnrest  15388  cnptopresti  15391  cnpdis  15395  lmtopcnp  15403  neitx  15421  tx1cn  15422  tx2cn  15423  txcnp  15424  txcnmpt  15426  txdis1cn  15431  psmetsym  15482  psmetres2  15486  isxmetd  15500  xmetsym  15521  xmetpsmet  15522  metrtri  15530  xblss2ps  15557  xblss2  15558  xblcntrps  15566  xblcntr  15567  bdxmet  15654  bdmet  15655  bdmopn  15657  xmetxp  15660  xmetxpbl  15661  rescncf  15734  cncfco  15744  mulcncflem  15760  mulcncf  15761  suplociccreex  15777  ivthinclemlopn  15789  ivthinclemuopn  15791  hovera  15800  hoverlt1  15802  cnplimcim  15820  cnplimclemr  15822  limccnpcntop  15828  limccnp2cntop  15830  limccoap  15831  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvcn  15853  dvaddxxbr  15854  dvmulxxbr  15855  dvcoapbr  15860  dvcjbr  15861  dvrecap  15866  rpabscxpbnd  16098  dvdsppwf1o  16205  chtqub  16218  bposlem1  16233  bposlem2  16234  lgsdirprm  16275  lgseisenlem1  16311  lgseisenlem2  16312  lgseisenlem3  16313  lgsquadlem1  16318  2sqlem8  16364  uspgr2wlkeq2  16729  clwwlknccat  16786  clwwlknonex2lem2  16801  eupthres  16820  refeq  17195  apdifflemf  17217  ltlenmkv  17242