Theorem mpbir2and 957

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  3818  isfsuppd  7283  nnnninfeq2  7462  nqnq0pi  7798  genpassg  7886  addnqpr  7921  mulnqpr  7937  distrprg  7948  1idpr  7952  ltexpri  7973  recexprlemex  7997  aptipr  8001  cauappcvgprlemladd  8018  letrid  8435  ltntri  8447  add20  8795  inelr  8905  recgt0  9173  prodgt0  9175  squeeze0  9227  suprzclex  9726  eluzadd  9933  eluzsub  9934  xrletrid  10189  xrre  10204  xrre3  10206  xleadd1a  10257  elioc2  10320  elico2  10321  elicc2  10322  elfz1eq  10421  fztri3or  10425  fzspl  10457  fznatpl1  10464  nn0fz0  10507  fzctr  10521  fzo1fzo0n0  10576  fzoaddel  10586  elincfzoext  10592  zsupcllemstep  10643  zssinfcl  10646  exbtwnz  10666  flid  10700  flqaddz  10713  flqdiv  10739  modqid  10767  frec2uzf1od  10824  iseqf1olemqk  10925  bcval5  11182  hashf1lem1  11266  eqs1  11377  pfxccatin12d  11498  abs2difabs  11855  fzomaxdiflem  11859  icodiamlt  11927  dfabsmax  11964  rexico  11968  mul0inf  11988  xrbdtri  12023  sumeq2  12106  sumsnf  12157  fsum00  12210  prodeq2  12305  prodsnf  12340  bitsfzolem  12702  bitsfzo  12703  bitsmod  12704  bitscmp  12706  gcd0id  12737  gcdneg  12740  nn0seqcvgd  12800  lcmval  12822  lcmneg  12833  qredeq  12855  prmind2  12879  pw2dvdseu  12927  pcpremul  13053  pcidlem  13083  pcgcd1  13088  fldivp1  13108  pcfaclem  13109  4sqlem17  13167  ballotfilemfc0  13213  ballotfilemfcc  13214  ennnfonelemex  13286  ennnfonelemnn0  13294  mnd1  13742  grp1  13891  0subg  13982  nmznsg  13996  ghmpreima  14049  ghmeql  14050  ghmnsgpreima  14052  kerf1ghm  14057  ring1  14340  dvdsrmuld  14379  1unit  14390  unitmulcl  14396  unitgrp  14399  unitnegcl  14413  rhmdvdsr  14458  elrhmunit  14460  subrngintm  14496  subrguss  14520  subrgunit  14523  rhmeql  14534  rhmima  14535  lsslsp  14741  rnglidlrng  14810  fczpsrbag  14982  psrbaglecl  14986  psrbagcon  14988  mplsubgfilemm  15015  mplsubgfilemcl  15016  mplsubgfileminv  15017  tgcl  15091  distop  15112  epttop  15117  neiss  15177  opnneissb  15182  ssnei2  15184  innei  15190  lmconst  15243  cnpnei  15246  cnptopco  15249  cnss1  15253  cnss2  15254  cncnpi  15255  cncnp  15257  cnconst2  15260  cnrest  15262  cnptopresti  15265  cnpdis  15269  lmtopcnp  15277  neitx  15295  tx1cn  15296  tx2cn  15297  txcnp  15298  txcnmpt  15300  txdis1cn  15305  psmetsym  15356  psmetres2  15360  isxmetd  15374  xmetsym  15395  xmetpsmet  15396  metrtri  15404  xblss2ps  15431  xblss2  15432  xblcntrps  15440  xblcntr  15441  bdxmet  15528  bdmet  15529  bdmopn  15531  xmetxp  15534  xmetxpbl  15535  rescncf  15608  cncfco  15618  mulcncflem  15634  mulcncf  15635  suplociccreex  15651  ivthinclemlopn  15663  ivthinclemuopn  15665  hovera  15674  hoverlt1  15676  cnplimcim  15694  cnplimclemr  15696  limccnpcntop  15702  limccnp2cntop  15704  limccoap  15705  dvidlemap  15718  dvidrelem  15719  dvidsslem  15720  dvcn  15727  dvaddxxbr  15728  dvmulxxbr  15729  dvcoapbr  15734  dvcjbr  15735  dvrecap  15740  rpabscxpbnd  15968  dvdsppwf1o  16020  lgsdirprm  16070  lgseisenlem1  16106  lgseisenlem2  16107  lgseisenlem3  16108  lgsquadlem1  16113  2sqlem8  16159  uspgr2wlkeq2  16524  clwwlknccat  16581  clwwlknonex2lem2  16596  eupthres  16615  refeq  16981  apdifflemf  17003  ltlenmkv  17028