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	⊢ (𝜑 → 𝜒)
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:  ifpprsnssdc  3774  nnnninfeq2  7312  nqnq0pi  7641  genpassg  7729  addnqpr  7764  mulnqpr  7780  distrprg  7791  1idpr  7795  ltexpri  7816  recexprlemex  7840  aptipr  7844  cauappcvgprlemladd  7861  ltntri  8290  add20  8637  inelr  8747  recgt0  9013  prodgt0  9015  squeeze0  9067  suprzclex  9561  eluzadd  9768  eluzsub  9769  xrletrid  10018  xrre  10033  xrre3  10035  xleadd1a  10086  elioc2  10149  elico2  10150  elicc2  10151  elfz1eq  10248  fztri3or  10252  fznatpl1  10289  nn0fz0  10332  fzctr  10346  fzo1fzo0n0  10400  fzoaddel  10410  elincfzoext  10416  zsupcllemstep  10466  zssinfcl  10469  exbtwnz  10487  flid  10521  flqaddz  10534  flqdiv  10560  modqid  10588  frec2uzf1od  10645  iseqf1olemqk  10746  bcval5  11002  eqs1  11181  pfxccatin12d  11298  abs2difabs  11640  fzomaxdiflem  11644  icodiamlt  11712  dfabsmax  11749  rexico  11753  mul0inf  11773  xrbdtri  11808  sumeq2  11891  sumsnf  11941  fsum00  11994  prodeq2  12089  prodsnf  12124  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  bitscmp  12490  gcd0id  12521  gcdneg  12524  nn0seqcvgd  12584  lcmval  12606  lcmneg  12617  qredeq  12639  prmind2  12663  pw2dvdseu  12711  hashdvds  12764  pcpremul  12837  pcidlem  12867  pcgcd1  12872  fldivp1  12892  pcfaclem  12893  4sqlem17  12951  ennnfonelemex  13006  ennnfonelemnn0  13014  mnd1  13509  grp1  13660  0subg  13757  nmznsg  13771  ghmpreima  13824  ghmeql  13825  ghmnsgpreima  13827  kerf1ghm  13832  ring1  14043  dvdsrmuld  14081  1unit  14092  unitmulcl  14098  unitgrp  14101  unitnegcl  14115  rhmdvdsr  14160  elrhmunit  14162  subrngintm  14197  subrguss  14221  subrgunit  14224  rhmeql  14235  rhmima  14236  lsslsp  14414  rnglidlrng  14483  fczpsrbag  14656  mplsubgfilemm  14683  mplsubgfilemcl  14684  mplsubgfileminv  14685  tgcl  14759  distop  14780  epttop  14785  neiss  14845  opnneissb  14850  ssnei2  14852  innei  14858  lmconst  14911  cnpnei  14914  cnptopco  14917  cnss1  14921  cnss2  14922  cncnpi  14923  cncnp  14925  cnconst2  14928  cnrest  14930  cnptopresti  14933  cnpdis  14937  lmtopcnp  14945  neitx  14963  tx1cn  14964  tx2cn  14965  txcnp  14966  txcnmpt  14968  txdis1cn  14973  psmetsym  15024  psmetres2  15028  isxmetd  15042  xmetsym  15063  xmetpsmet  15064  metrtri  15072  xblss2ps  15099  xblss2  15100  xblcntrps  15108  xblcntr  15109  bdxmet  15196  bdmet  15197  bdmopn  15199  xmetxp  15202  xmetxpbl  15203  rescncf  15276  cncfco  15286  mulcncflem  15302  mulcncf  15303  suplociccreex  15319  ivthinclemlopn  15331  ivthinclemuopn  15333  hovera  15342  hoverlt1  15344  cnplimcim  15362  cnplimclemr  15364  limccnpcntop  15370  limccnp2cntop  15372  limccoap  15373  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvcn  15395  dvaddxxbr  15396  dvmulxxbr  15397  dvcoapbr  15402  dvcjbr  15403  dvrecap  15408  rpabscxpbnd  15635  dvdsppwf1o  15684  lgsdirprm  15734  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgsquadlem1  15777  2sqlem8  15823  uspgr2wlkeq2  16138  clwwlknccat  16191  refeq  16510  apdifflemf  16528  ltlenmkv  16552