Theorem mpbir2and 953

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  3798  isfsuppd  7242  nnnninfeq2  7419  nqnq0pi  7749  genpassg  7837  addnqpr  7872  mulnqpr  7888  distrprg  7899  1idpr  7903  ltexpri  7924  recexprlemex  7948  aptipr  7952  cauappcvgprlemladd  7969  ltntri  8397  add20  8744  inelr  8854  recgt0  9120  prodgt0  9122  squeeze0  9174  suprzclex  9672  eluzadd  9879  eluzsub  9880  xrletrid  10134  xrre  10149  xrre3  10151  xleadd1a  10202  elioc2  10265  elico2  10266  elicc2  10267  elfz1eq  10365  fztri3or  10369  fznatpl1  10406  nn0fz0  10449  fzctr  10463  fzo1fzo0n0  10518  fzoaddel  10528  elincfzoext  10534  zsupcllemstep  10585  zssinfcl  10588  exbtwnz  10606  flid  10640  flqaddz  10653  flqdiv  10679  modqid  10707  frec2uzf1od  10764  iseqf1olemqk  10865  bcval5  11121  eqs1  11309  pfxccatin12d  11430  abs2difabs  11786  fzomaxdiflem  11790  icodiamlt  11858  dfabsmax  11895  rexico  11899  mul0inf  11919  xrbdtri  11954  sumeq2  12037  sumsnf  12088  fsum00  12141  prodeq2  12236  prodsnf  12271  bitsfzolem  12633  bitsfzo  12634  bitsmod  12635  bitscmp  12637  gcd0id  12668  gcdneg  12671  nn0seqcvgd  12731  lcmval  12753  lcmneg  12764  qredeq  12786  prmind2  12810  pw2dvdseu  12858  pcpremul  12984  pcidlem  13014  pcgcd1  13019  fldivp1  13039  pcfaclem  13040  4sqlem17  13098  ennnfonelemex  13154  ennnfonelemnn0  13162  mnd1  13657  grp1  13808  0subg  13905  nmznsg  13919  ghmpreima  13972  ghmeql  13973  ghmnsgpreima  13975  kerf1ghm  13980  ring1  14192  dvdsrmuld  14230  1unit  14241  unitmulcl  14247  unitgrp  14250  unitnegcl  14264  rhmdvdsr  14309  elrhmunit  14311  subrngintm  14346  subrguss  14370  subrgunit  14373  rhmeql  14384  rhmima  14385  lsslsp  14564  rnglidlrng  14633  fczpsrbag  14807  psrbaglecl  14811  psrbagcon  14813  mplsubgfilemm  14840  mplsubgfilemcl  14841  mplsubgfileminv  14842  tgcl  14916  distop  14937  epttop  14942  neiss  15002  opnneissb  15007  ssnei2  15009  innei  15015  lmconst  15068  cnpnei  15071  cnptopco  15074  cnss1  15078  cnss2  15079  cncnpi  15080  cncnp  15082  cnconst2  15085  cnrest  15087  cnptopresti  15090  cnpdis  15094  lmtopcnp  15102  neitx  15120  tx1cn  15121  tx2cn  15122  txcnp  15123  txcnmpt  15125  txdis1cn  15130  psmetsym  15181  psmetres2  15185  isxmetd  15199  xmetsym  15220  xmetpsmet  15221  metrtri  15229  xblss2ps  15256  xblss2  15257  xblcntrps  15265  xblcntr  15266  bdxmet  15353  bdmet  15354  bdmopn  15356  xmetxp  15359  xmetxpbl  15360  rescncf  15433  cncfco  15443  mulcncflem  15459  mulcncf  15460  suplociccreex  15476  ivthinclemlopn  15488  ivthinclemuopn  15490  hovera  15499  hoverlt1  15501  cnplimcim  15519  cnplimclemr  15521  limccnpcntop  15527  limccnp2cntop  15529  limccoap  15530  dvidlemap  15543  dvidrelem  15544  dvidsslem  15545  dvcn  15552  dvaddxxbr  15553  dvmulxxbr  15554  dvcoapbr  15559  dvcjbr  15560  dvrecap  15565  rpabscxpbnd  15792  dvdsppwf1o  15844  lgsdirprm  15894  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgsquadlem1  15937  2sqlem8  15983  uspgr2wlkeq2  16348  clwwlknccat  16405  clwwlknonex2lem2  16420  eupthres  16439  refeq  16795  apdifflemf  16817  ltlenmkv  16842