Theorem mpbir2and 944

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  7117  nqnq0pi  7412  genpassg  7500  addnqpr  7535  mulnqpr  7551  distrprg  7562  1idpr  7566  ltexpri  7587  recexprlemex  7611  aptipr  7615  cauappcvgprlemladd  7632  ltntri  8059  add20  8405  inelr  8515  recgt0  8778  prodgt0  8780  squeeze0  8832  suprzclex  9322  eluzadd  9527  eluzsub  9528  xrletrid  9774  xrre  9789  xrre3  9791  xleadd1a  9842  elioc2  9905  elico2  9906  elicc2  9907  elfz1eq  10003  fztri3or  10007  fznatpl1  10044  nn0fz0  10087  fzctr  10101  fzo1fzo0n0  10151  fzoaddel  10160  exbtwnz  10219  flid  10252  flqaddz  10265  flqdiv  10289  modqid  10317  frec2uzf1od  10374  iseqf1olemqk  10462  bcval5  10709  abs2difabs  11083  fzomaxdiflem  11087  icodiamlt  11155  dfabsmax  11192  rexico  11196  mul0inf  11215  xrbdtri  11250  sumeq2  11333  sumsnf  11383  fsum00  11436  prodeq2  11531  prodsnf  11566  zsupcllemstep  11911  zssinfcl  11914  gcd0id  11945  gcdneg  11948  nn0seqcvgd  12006  lcmval  12028  lcmneg  12039  qredeq  12061  prmind2  12085  pw2dvdseu  12133  hashdvds  12186  pcpremul  12258  pcidlem  12287  pcgcd1  12292  fldivp1  12311  pcfaclem  12312  ennnfonelemex  12380  ennnfonelemnn0  12388  mnd1  12708  grp1  12835  ring1  13030  tgcl  13133  distop  13154  epttop  13159  neiss  13219  opnneissb  13224  ssnei2  13226  innei  13232  lmconst  13285  cnpnei  13288  cnptopco  13291  cnss1  13295  cnss2  13296  cncnpi  13297  cncnp  13299  cnconst2  13302  cnrest  13304  cnptopresti  13307  cnpdis  13311  lmtopcnp  13319  neitx  13337  tx1cn  13338  tx2cn  13339  txcnp  13340  txcnmpt  13342  txdis1cn  13347  psmetsym  13398  psmetres2  13402  isxmetd  13416  xmetsym  13437  xmetpsmet  13438  metrtri  13446  xblss2ps  13473  xblss2  13474  xblcntrps  13482  xblcntr  13483  bdxmet  13570  bdmet  13571  bdmopn  13573  xmetxp  13576  xmetxpbl  13577  rescncf  13637  cncfco  13647  mulcncflem  13659  mulcncf  13660  suplociccreex  13671  ivthinclemlopn  13683  ivthinclemuopn  13685  cnplimcim  13705  cnplimclemr  13707  limccnpcntop  13713  limccnp2cntop  13715  limccoap  13716  dvidlemap  13729  dvcn  13733  dvaddxxbr  13734  dvmulxxbr  13735  dvcoapbr  13740  dvcjbr  13741  dvrecap  13746  rpabscxpbnd  13928  lgsdirprm  14004  2sqlem8  14028  refeq  14335  apdifflemf  14353