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	⊢ (𝜑 → 𝜒)
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  7147  nqnq0pi  7457  genpassg  7545  addnqpr  7580  mulnqpr  7596  distrprg  7607  1idpr  7611  ltexpri  7632  recexprlemex  7656  aptipr  7660  cauappcvgprlemladd  7677  ltntri  8105  add20  8451  inelr  8561  recgt0  8827  prodgt0  8829  squeeze0  8881  suprzclex  9371  eluzadd  9576  eluzsub  9577  xrletrid  9825  xrre  9840  xrre3  9842  xleadd1a  9893  elioc2  9956  elico2  9957  elicc2  9958  elfz1eq  10055  fztri3or  10059  fznatpl1  10096  nn0fz0  10139  fzctr  10153  fzo1fzo0n0  10203  fzoaddel  10212  exbtwnz  10271  flid  10304  flqaddz  10317  flqdiv  10341  modqid  10369  frec2uzf1od  10426  iseqf1olemqk  10514  bcval5  10763  abs2difabs  11137  fzomaxdiflem  11141  icodiamlt  11209  dfabsmax  11246  rexico  11250  mul0inf  11269  xrbdtri  11304  sumeq2  11387  sumsnf  11437  fsum00  11490  prodeq2  11585  prodsnf  11620  zsupcllemstep  11966  zssinfcl  11969  gcd0id  12000  gcdneg  12003  nn0seqcvgd  12061  lcmval  12083  lcmneg  12094  qredeq  12116  prmind2  12140  pw2dvdseu  12188  hashdvds  12241  pcpremul  12313  pcidlem  12342  pcgcd1  12347  fldivp1  12366  pcfaclem  12367  ennnfonelemex  12440  ennnfonelemnn0  12448  mnd1  12880  grp1  13023  0subg  13111  nmznsg  13125  ghmpreima  13173  ghmeql  13174  ghmnsgpreima  13176  kerf1ghm  13181  ring1  13379  dvdsrmuld  13414  1unit  13425  unitmulcl  13431  unitgrp  13434  unitnegcl  13448  rhmdvdsr  13493  elrhmunit  13495  subrngintm  13527  subrguss  13551  subrgunit  13554  lsslsp  13713  rnglidlrng  13782  tgcl  13968  distop  13989  epttop  13994  neiss  14054  opnneissb  14059  ssnei2  14061  innei  14067  lmconst  14120  cnpnei  14123  cnptopco  14126  cnss1  14130  cnss2  14131  cncnpi  14132  cncnp  14134  cnconst2  14137  cnrest  14139  cnptopresti  14142  cnpdis  14146  lmtopcnp  14154  neitx  14172  tx1cn  14173  tx2cn  14174  txcnp  14175  txcnmpt  14177  txdis1cn  14182  psmetsym  14233  psmetres2  14237  isxmetd  14251  xmetsym  14272  xmetpsmet  14273  metrtri  14281  xblss2ps  14308  xblss2  14309  xblcntrps  14317  xblcntr  14318  bdxmet  14405  bdmet  14406  bdmopn  14408  xmetxp  14411  xmetxpbl  14412  rescncf  14472  cncfco  14482  mulcncflem  14494  mulcncf  14495  suplociccreex  14506  ivthinclemlopn  14518  ivthinclemuopn  14520  cnplimcim  14540  cnplimclemr  14542  limccnpcntop  14548  limccnp2cntop  14550  limccoap  14551  dvidlemap  14564  dvcn  14568  dvaddxxbr  14569  dvmulxxbr  14570  dvcoapbr  14575  dvcjbr  14576  dvrecap  14581  rpabscxpbnd  14763  lgsdirprm  14839  lgseisenlem1  14854  lgseisenlem2  14855  2sqlem8  14874  refeq  15181  apdifflemf  15199  ltlenmkv  15223