Theorem mpbir2and 946

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  7195  nqnq0pi  7505  genpassg  7593  addnqpr  7628  mulnqpr  7644  distrprg  7655  1idpr  7659  ltexpri  7680  recexprlemex  7704  aptipr  7708  cauappcvgprlemladd  7725  ltntri  8154  add20  8501  inelr  8611  recgt0  8877  prodgt0  8879  squeeze0  8931  suprzclex  9424  eluzadd  9630  eluzsub  9631  xrletrid  9880  xrre  9895  xrre3  9897  xleadd1a  9948  elioc2  10011  elico2  10012  elicc2  10013  elfz1eq  10110  fztri3or  10114  fznatpl1  10151  nn0fz0  10194  fzctr  10208  fzo1fzo0n0  10259  fzoaddel  10268  zsupcllemstep  10319  zssinfcl  10322  exbtwnz  10340  flid  10374  flqaddz  10387  flqdiv  10413  modqid  10441  frec2uzf1od  10498  iseqf1olemqk  10599  bcval5  10855  abs2difabs  11273  fzomaxdiflem  11277  icodiamlt  11345  dfabsmax  11382  rexico  11386  mul0inf  11406  xrbdtri  11441  sumeq2  11524  sumsnf  11574  fsum00  11627  prodeq2  11722  prodsnf  11757  bitsfzolem  12118  bitsfzo  12119  gcd0id  12146  gcdneg  12149  nn0seqcvgd  12209  lcmval  12231  lcmneg  12242  qredeq  12264  prmind2  12288  pw2dvdseu  12336  hashdvds  12389  pcpremul  12462  pcidlem  12492  pcgcd1  12497  fldivp1  12517  pcfaclem  12518  4sqlem17  12576  ennnfonelemex  12631  ennnfonelemnn0  12639  mnd1  13087  grp1  13238  0subg  13329  nmznsg  13343  ghmpreima  13396  ghmeql  13397  ghmnsgpreima  13399  kerf1ghm  13404  ring1  13615  dvdsrmuld  13652  1unit  13663  unitmulcl  13669  unitgrp  13672  unitnegcl  13686  rhmdvdsr  13731  elrhmunit  13733  subrngintm  13768  subrguss  13792  subrgunit  13795  rhmeql  13806  rhmima  13807  lsslsp  13985  rnglidlrng  14054  fczpsrbag  14225  tgcl  14300  distop  14321  epttop  14326  neiss  14386  opnneissb  14391  ssnei2  14393  innei  14399  lmconst  14452  cnpnei  14455  cnptopco  14458  cnss1  14462  cnss2  14463  cncnpi  14464  cncnp  14466  cnconst2  14469  cnrest  14471  cnptopresti  14474  cnpdis  14478  lmtopcnp  14486  neitx  14504  tx1cn  14505  tx2cn  14506  txcnp  14507  txcnmpt  14509  txdis1cn  14514  psmetsym  14565  psmetres2  14569  isxmetd  14583  xmetsym  14604  xmetpsmet  14605  metrtri  14613  xblss2ps  14640  xblss2  14641  xblcntrps  14649  xblcntr  14650  bdxmet  14737  bdmet  14738  bdmopn  14740  xmetxp  14743  xmetxpbl  14744  rescncf  14817  cncfco  14827  mulcncflem  14843  mulcncf  14844  suplociccreex  14860  ivthinclemlopn  14872  ivthinclemuopn  14874  hovera  14883  hoverlt1  14885  cnplimcim  14903  cnplimclemr  14905  limccnpcntop  14911  limccnp2cntop  14913  limccoap  14914  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvcn  14936  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvrecap  14949  rpabscxpbnd  15176  dvdsppwf1o  15225  lgsdirprm  15275  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgsquadlem1  15318  2sqlem8  15364  refeq  15672  apdifflemf  15690  ltlenmkv  15714