Theorem mpbir2and 950

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  7284  nqnq0pi  7613  genpassg  7701  addnqpr  7736  mulnqpr  7752  distrprg  7763  1idpr  7767  ltexpri  7788  recexprlemex  7812  aptipr  7816  cauappcvgprlemladd  7833  ltntri  8262  add20  8609  inelr  8719  recgt0  8985  prodgt0  8987  squeeze0  9039  suprzclex  9533  eluzadd  9739  eluzsub  9740  xrletrid  9989  xrre  10004  xrre3  10006  xleadd1a  10057  elioc2  10120  elico2  10121  elicc2  10122  elfz1eq  10219  fztri3or  10223  fznatpl1  10260  nn0fz0  10303  fzctr  10317  fzo1fzo0n0  10371  fzoaddel  10380  elincfzoext  10386  zsupcllemstep  10436  zssinfcl  10439  exbtwnz  10457  flid  10491  flqaddz  10504  flqdiv  10530  modqid  10558  frec2uzf1od  10615  iseqf1olemqk  10716  bcval5  10972  eqs1  11147  pfxccatin12d  11263  abs2difabs  11605  fzomaxdiflem  11609  icodiamlt  11677  dfabsmax  11714  rexico  11718  mul0inf  11738  xrbdtri  11773  sumeq2  11856  sumsnf  11906  fsum00  11959  prodeq2  12054  prodsnf  12089  bitsfzolem  12451  bitsfzo  12452  bitsmod  12453  bitscmp  12455  gcd0id  12486  gcdneg  12489  nn0seqcvgd  12549  lcmval  12571  lcmneg  12582  qredeq  12604  prmind2  12628  pw2dvdseu  12676  hashdvds  12729  pcpremul  12802  pcidlem  12832  pcgcd1  12837  fldivp1  12857  pcfaclem  12858  4sqlem17  12916  ennnfonelemex  12971  ennnfonelemnn0  12979  mnd1  13474  grp1  13625  0subg  13722  nmznsg  13736  ghmpreima  13789  ghmeql  13790  ghmnsgpreima  13792  kerf1ghm  13797  ring1  14008  dvdsrmuld  14045  1unit  14056  unitmulcl  14062  unitgrp  14065  unitnegcl  14079  rhmdvdsr  14124  elrhmunit  14126  subrngintm  14161  subrguss  14185  subrgunit  14188  rhmeql  14199  rhmima  14200  lsslsp  14378  rnglidlrng  14447  fczpsrbag  14620  mplsubgfilemm  14647  mplsubgfilemcl  14648  mplsubgfileminv  14649  tgcl  14723  distop  14744  epttop  14749  neiss  14809  opnneissb  14814  ssnei2  14816  innei  14822  lmconst  14875  cnpnei  14878  cnptopco  14881  cnss1  14885  cnss2  14886  cncnpi  14887  cncnp  14889  cnconst2  14892  cnrest  14894  cnptopresti  14897  cnpdis  14901  lmtopcnp  14909  neitx  14927  tx1cn  14928  tx2cn  14929  txcnp  14930  txcnmpt  14932  txdis1cn  14937  psmetsym  14988  psmetres2  14992  isxmetd  15006  xmetsym  15027  xmetpsmet  15028  metrtri  15036  xblss2ps  15063  xblss2  15064  xblcntrps  15072  xblcntr  15073  bdxmet  15160  bdmet  15161  bdmopn  15163  xmetxp  15166  xmetxpbl  15167  rescncf  15240  cncfco  15250  mulcncflem  15266  mulcncf  15267  suplociccreex  15283  ivthinclemlopn  15295  ivthinclemuopn  15297  hovera  15306  hoverlt1  15308  cnplimcim  15326  cnplimclemr  15328  limccnpcntop  15334  limccnp2cntop  15336  limccoap  15337  dvidlemap  15350  dvidrelem  15351  dvidsslem  15352  dvcn  15359  dvaddxxbr  15360  dvmulxxbr  15361  dvcoapbr  15366  dvcjbr  15367  dvrecap  15372  rpabscxpbnd  15599  dvdsppwf1o  15648  lgsdirprm  15698  lgseisenlem1  15734  lgseisenlem2  15735  lgseisenlem3  15736  lgsquadlem1  15741  2sqlem8  15787  refeq  16327  apdifflemf  16345  ltlenmkv  16369