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  3804  isfsuppd  7256  nnnninfeq2  7433  nqnq0pi  7769  genpassg  7857  addnqpr  7892  mulnqpr  7908  distrprg  7919  1idpr  7923  ltexpri  7944  recexprlemex  7968  aptipr  7972  cauappcvgprlemladd  7989  ltntri  8417  add20  8765  inelr  8875  recgt0  9141  prodgt0  9143  squeeze0  9195  suprzclex  9694  eluzadd  9901  eluzsub  9902  xrletrid  10157  xrre  10172  xrre3  10174  xleadd1a  10225  elioc2  10288  elico2  10289  elicc2  10290  elfz1eq  10389  fztri3or  10393  fzspl  10425  fznatpl1  10432  nn0fz0  10475  fzctr  10489  fzo1fzo0n0  10544  fzoaddel  10554  elincfzoext  10560  zsupcllemstep  10611  zssinfcl  10614  exbtwnz  10634  flid  10668  flqaddz  10681  flqdiv  10707  modqid  10735  frec2uzf1od  10792  iseqf1olemqk  10893  bcval5  11150  eqs1  11341  pfxccatin12d  11462  abs2difabs  11818  fzomaxdiflem  11822  icodiamlt  11890  dfabsmax  11927  rexico  11931  mul0inf  11951  xrbdtri  11986  sumeq2  12069  sumsnf  12120  fsum00  12173  prodeq2  12268  prodsnf  12303  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitscmp  12669  gcd0id  12700  gcdneg  12703  nn0seqcvgd  12763  lcmval  12785  lcmneg  12796  qredeq  12818  prmind2  12842  pw2dvdseu  12890  pcpremul  13016  pcidlem  13046  pcgcd1  13051  fldivp1  13071  pcfaclem  13072  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemex  13249  ennnfonelemnn0  13257  mnd1  13752  grp1  13903  0subg  14000  nmznsg  14014  ghmpreima  14067  ghmeql  14068  ghmnsgpreima  14070  kerf1ghm  14075  ring1  14287  dvdsrmuld  14326  1unit  14337  unitmulcl  14343  unitgrp  14346  unitnegcl  14360  rhmdvdsr  14405  elrhmunit  14407  subrngintm  14443  subrguss  14467  subrgunit  14470  rhmeql  14481  rhmima  14482  lsslsp  14689  rnglidlrng  14758  fczpsrbag  14932  psrbaglecl  14936  psrbagcon  14938  mplsubgfilemm  14965  mplsubgfilemcl  14966  mplsubgfileminv  14967  tgcl  15041  distop  15062  epttop  15067  neiss  15127  opnneissb  15132  ssnei2  15134  innei  15140  lmconst  15193  cnpnei  15196  cnptopco  15199  cnss1  15203  cnss2  15204  cncnpi  15205  cncnp  15207  cnconst2  15210  cnrest  15212  cnptopresti  15215  cnpdis  15219  lmtopcnp  15227  neitx  15245  tx1cn  15246  tx2cn  15247  txcnp  15248  txcnmpt  15250  txdis1cn  15255  psmetsym  15306  psmetres2  15310  isxmetd  15324  xmetsym  15345  xmetpsmet  15346  metrtri  15354  xblss2ps  15381  xblss2  15382  xblcntrps  15390  xblcntr  15391  bdxmet  15478  bdmet  15479  bdmopn  15481  xmetxp  15484  xmetxpbl  15485  rescncf  15558  cncfco  15568  mulcncflem  15584  mulcncf  15585  suplociccreex  15601  ivthinclemlopn  15613  ivthinclemuopn  15615  hovera  15624  hoverlt1  15626  cnplimcim  15644  cnplimclemr  15646  limccnpcntop  15652  limccnp2cntop  15654  limccoap  15655  dvidlemap  15668  dvidrelem  15669  dvidsslem  15670  dvcn  15677  dvaddxxbr  15678  dvmulxxbr  15679  dvcoapbr  15684  dvcjbr  15685  dvrecap  15690  rpabscxpbnd  15917  dvdsppwf1o  15969  lgsdirprm  16019  lgseisenlem1  16055  lgseisenlem2  16056  lgseisenlem3  16057  lgsquadlem1  16062  2sqlem8  16108  uspgr2wlkeq2  16473  clwwlknccat  16530  clwwlknonex2lem2  16545  eupthres  16564  refeq  16920  apdifflemf  16942  ltlenmkv  16968