Theorem mpbir2and 949

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	⊢ (𝜑 → 𝜒)
mpbir2and.2	⊢ (𝜑 → 𝜃)
mpbir2and.3	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
mpbir2and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir2and

Step	Hyp	Ref	Expression
1		mpbir2and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir2and.2	. . 3 ⊢ (𝜑 → 𝜃)
3	1, 2	jca 306	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 167	1 ⊢ (𝜑 → 𝜓)

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  7264  nqnq0pi  7593  genpassg  7681  addnqpr  7716  mulnqpr  7732  distrprg  7743  1idpr  7747  ltexpri  7768  recexprlemex  7792  aptipr  7796  cauappcvgprlemladd  7813  ltntri  8242  add20  8589  inelr  8699  recgt0  8965  prodgt0  8967  squeeze0  9019  suprzclex  9513  eluzadd  9719  eluzsub  9720  xrletrid  9969  xrre  9984  xrre3  9986  xleadd1a  10037  elioc2  10100  elico2  10101  elicc2  10102  elfz1eq  10199  fztri3or  10203  fznatpl1  10240  nn0fz0  10283  fzctr  10297  fzo1fzo0n0  10351  fzoaddel  10360  elincfzoext  10366  zsupcllemstep  10416  zssinfcl  10419  exbtwnz  10437  flid  10471  flqaddz  10484  flqdiv  10510  modqid  10538  frec2uzf1od  10595  iseqf1olemqk  10696  bcval5  10952  eqs1  11127  pfxccatin12d  11243  abs2difabs  11585  fzomaxdiflem  11589  icodiamlt  11657  dfabsmax  11694  rexico  11698  mul0inf  11718  xrbdtri  11753  sumeq2  11836  sumsnf  11886  fsum00  11939  prodeq2  12034  prodsnf  12069  bitsfzolem  12431  bitsfzo  12432  bitsmod  12433  bitscmp  12435  gcd0id  12466  gcdneg  12469  nn0seqcvgd  12529  lcmval  12551  lcmneg  12562  qredeq  12584  prmind2  12608  pw2dvdseu  12656  hashdvds  12709  pcpremul  12782  pcidlem  12812  pcgcd1  12817  fldivp1  12837  pcfaclem  12838  4sqlem17  12896  ennnfonelemex  12951  ennnfonelemnn0  12959  mnd1  13454  grp1  13605  0subg  13702  nmznsg  13716  ghmpreima  13769  ghmeql  13770  ghmnsgpreima  13772  kerf1ghm  13777  ring1  13988  dvdsrmuld  14025  1unit  14036  unitmulcl  14042  unitgrp  14045  unitnegcl  14059  rhmdvdsr  14104  elrhmunit  14106  subrngintm  14141  subrguss  14165  subrgunit  14168  rhmeql  14179  rhmima  14180  lsslsp  14358  rnglidlrng  14427  fczpsrbag  14600  mplsubgfilemm  14627  mplsubgfilemcl  14628  mplsubgfileminv  14629  tgcl  14703  distop  14724  epttop  14729  neiss  14789  opnneissb  14794  ssnei2  14796  innei  14802  lmconst  14855  cnpnei  14858  cnptopco  14861  cnss1  14865  cnss2  14866  cncnpi  14867  cncnp  14869  cnconst2  14872  cnrest  14874  cnptopresti  14877  cnpdis  14881  lmtopcnp  14889  neitx  14907  tx1cn  14908  tx2cn  14909  txcnp  14910  txcnmpt  14912  txdis1cn  14917  psmetsym  14968  psmetres2  14972  isxmetd  14986  xmetsym  15007  xmetpsmet  15008  metrtri  15016  xblss2ps  15043  xblss2  15044  xblcntrps  15052  xblcntr  15053  bdxmet  15140  bdmet  15141  bdmopn  15143  xmetxp  15146  xmetxpbl  15147  rescncf  15220  cncfco  15230  mulcncflem  15246  mulcncf  15247  suplociccreex  15263  ivthinclemlopn  15275  ivthinclemuopn  15277  hovera  15286  hoverlt1  15288  cnplimcim  15306  cnplimclemr  15308  limccnpcntop  15314  limccnp2cntop  15316  limccoap  15317  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dvcn  15339  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvcjbr  15347  dvrecap  15352  rpabscxpbnd  15579  dvdsppwf1o  15628  lgsdirprm  15678  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem3  15716  lgsquadlem1  15721  2sqlem8  15767  refeq  16307  apdifflemf  16325  ltlenmkv  16349