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  7204  nqnq0pi  7522  genpassg  7610  addnqpr  7645  mulnqpr  7661  distrprg  7672  1idpr  7676  ltexpri  7697  recexprlemex  7721  aptipr  7725  cauappcvgprlemladd  7742  ltntri  8171  add20  8518  inelr  8628  recgt0  8894  prodgt0  8896  squeeze0  8948  suprzclex  9441  eluzadd  9647  eluzsub  9648  xrletrid  9897  xrre  9912  xrre3  9914  xleadd1a  9965  elioc2  10028  elico2  10029  elicc2  10030  elfz1eq  10127  fztri3or  10131  fznatpl1  10168  nn0fz0  10211  fzctr  10225  fzo1fzo0n0  10276  fzoaddel  10285  zsupcllemstep  10336  zssinfcl  10339  exbtwnz  10357  flid  10391  flqaddz  10404  flqdiv  10430  modqid  10458  frec2uzf1od  10515  iseqf1olemqk  10616  bcval5  10872  abs2difabs  11290  fzomaxdiflem  11294  icodiamlt  11362  dfabsmax  11399  rexico  11403  mul0inf  11423  xrbdtri  11458  sumeq2  11541  sumsnf  11591  fsum00  11644  prodeq2  11739  prodsnf  11774  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitscmp  12140  gcd0id  12171  gcdneg  12174  nn0seqcvgd  12234  lcmval  12256  lcmneg  12267  qredeq  12289  prmind2  12313  pw2dvdseu  12361  hashdvds  12414  pcpremul  12487  pcidlem  12517  pcgcd1  12522  fldivp1  12542  pcfaclem  12543  4sqlem17  12601  ennnfonelemex  12656  ennnfonelemnn0  12664  mnd1  13157  grp1  13308  0subg  13405  nmznsg  13419  ghmpreima  13472  ghmeql  13473  ghmnsgpreima  13475  kerf1ghm  13480  ring1  13691  dvdsrmuld  13728  1unit  13739  unitmulcl  13745  unitgrp  13748  unitnegcl  13762  rhmdvdsr  13807  elrhmunit  13809  subrngintm  13844  subrguss  13868  subrgunit  13871  rhmeql  13882  rhmima  13883  lsslsp  14061  rnglidlrng  14130  fczpsrbag  14301  tgcl  14384  distop  14405  epttop  14410  neiss  14470  opnneissb  14475  ssnei2  14477  innei  14483  lmconst  14536  cnpnei  14539  cnptopco  14542  cnss1  14546  cnss2  14547  cncnpi  14548  cncnp  14550  cnconst2  14553  cnrest  14555  cnptopresti  14558  cnpdis  14562  lmtopcnp  14570  neitx  14588  tx1cn  14589  tx2cn  14590  txcnp  14591  txcnmpt  14593  txdis1cn  14598  psmetsym  14649  psmetres2  14653  isxmetd  14667  xmetsym  14688  xmetpsmet  14689  metrtri  14697  xblss2ps  14724  xblss2  14725  xblcntrps  14733  xblcntr  14734  bdxmet  14821  bdmet  14822  bdmopn  14824  xmetxp  14827  xmetxpbl  14828  rescncf  14901  cncfco  14911  mulcncflem  14927  mulcncf  14928  suplociccreex  14944  ivthinclemlopn  14956  ivthinclemuopn  14958  hovera  14967  hoverlt1  14969  cnplimcim  14987  cnplimclemr  14989  limccnpcntop  14995  limccnp2cntop  14997  limccoap  14998  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcn  15020  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  rpabscxpbnd  15260  dvdsppwf1o  15309  lgsdirprm  15359  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgsquadlem1  15402  2sqlem8  15448  refeq  15759  apdifflemf  15777  ltlenmkv  15801