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  7284  nnnninfeq2  7463  nqnq0pi  7799  genpassg  7887  addnqpr  7922  mulnqpr  7938  distrprg  7949  1idpr  7953  ltexpri  7974  recexprlemex  7998  aptipr  8002  cauappcvgprlemladd  8019  letrid  8436  ltntri  8448  add20  8796  inelr  8906  recgt0  9174  prodgt0  9176  squeeze0  9228  suprzclex  9727  eluzadd  9934  eluzsub  9935  xrletrid  10190  xrre  10205  xrre3  10207  xleadd1a  10258  elioc2  10321  elico2  10322  elicc2  10323  elfz1eq  10422  fztri3or  10426  fzspl  10459  fznatpl1  10466  nn0fz0  10509  fzctr  10523  fzo1fzo0n0  10578  fzoaddel  10588  elincfzoext  10594  zsupcllemstep  10645  zssinfcl  10648  exbtwnz  10668  flid  10702  flqaddz  10715  flqdiv  10741  modqid  10769  frec2uzf1od  10826  iseqf1olemqk  10927  bcval5  11184  hashf1lem1  11268  eqs1  11379  pfxccatin12d  11500  abs2difabs  11857  fzomaxdiflem  11861  icodiamlt  11929  dfabsmax  11966  rexico  11970  mul0inf  11990  xrbdtri  12025  sumeq2  12108  sumsnf  12159  fsum00  12212  prodeq2  12307  prodsnf  12342  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitscmp  12708  gcd0id  12739  gcdneg  12742  nn0seqcvgd  12802  lcmval  12824  lcmneg  12835  qredeq  12857  prmind2  12881  pw2dvdseu  12929  pcpremul  13055  pcidlem  13085  pcgcd1  13090  fldivp1  13110  pcfaclem  13111  4sqlem17  13169  ballotfilemfc0  13215  ballotfilemfcc  13216  ennnfonelemex  13288  ennnfonelemnn0  13296  mnd1  13745  grp1  13894  0subg  13985  nmznsg  13999  ghmpreima  14052  ghmeql  14053  ghmnsgpreima  14055  kerf1ghm  14060  ring1  14347  dvdsrmuld  14386  1unit  14397  unitmulcl  14403  unitgrp  14406  unitnegcl  14420  rhmdvdsr  14465  elrhmunit  14467  subrngintm  14503  subrguss  14527  subrgunit  14530  rhmeql  14541  rhmima  14542  lsslsp  14749  rnglidlrng  14818  issubassa  14996  issubassa2  15018  fczpsrbag  15039  psrbaglecl  15043  psrbagcon  15045  mplsubgfilemm  15072  mplsubgfilemcl  15073  mplsubgfileminv  15074  tgcl  15148  distop  15169  epttop  15174  neiss  15234  opnneissb  15239  ssnei2  15241  innei  15247  lmconst  15300  cnpnei  15303  cnptopco  15306  cnss1  15310  cnss2  15311  cncnpi  15312  cncnp  15314  cnconst2  15317  cnrest  15319  cnptopresti  15322  cnpdis  15326  lmtopcnp  15334  neitx  15352  tx1cn  15353  tx2cn  15354  txcnp  15355  txcnmpt  15357  txdis1cn  15362  psmetsym  15413  psmetres2  15417  isxmetd  15431  xmetsym  15452  xmetpsmet  15453  metrtri  15461  xblss2ps  15488  xblss2  15489  xblcntrps  15497  xblcntr  15498  bdxmet  15585  bdmet  15586  bdmopn  15588  xmetxp  15591  xmetxpbl  15592  rescncf  15665  cncfco  15675  mulcncflem  15691  mulcncf  15692  suplociccreex  15708  ivthinclemlopn  15720  ivthinclemuopn  15722  hovera  15731  hoverlt1  15733  cnplimcim  15751  cnplimclemr  15753  limccnpcntop  15759  limccnp2cntop  15761  limccoap  15762  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvcn  15784  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcjbr  15792  dvrecap  15797  rpabscxpbnd  16025  dvdsppwf1o  16086  lgsdirprm  16136  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgsquadlem1  16179  2sqlem8  16225  uspgr2wlkeq2  16590  clwwlknccat  16647  clwwlknonex2lem2  16662  eupthres  16681  refeq  17047  apdifflemf  17069  ltlenmkv  17094