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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpprsnssdc  3820  isfsuppd  7290  nnnninfeq2  7469  nqnq0pi  7805  genpassg  7893  addnqpr  7928  mulnqpr  7944  distrprg  7955  1idpr  7959  ltexpri  7980  recexprlemex  8004  aptipr  8008  cauappcvgprlemladd  8025  letrid  8443  ltntri  8455  add20  8803  inelr  8914  recgt0  9182  prodgt0  9184  squeeze0  9236  suprzclex  9748  eluzadd  9960  eluzsub  9961  xrletrid  10217  xrre  10232  xrre3  10234  xleadd1a  10285  elioc2  10348  elico2  10349  elicc2  10350  elfz1eq  10449  fztri3or  10453  fzspl  10486  fznatpl1  10493  nn0fz0  10536  fzctr  10550  fzo1fzo0n0  10605  fzoaddel  10615  elincfzoext  10621  zsupcllemstep  10672  zssinfcl  10675  exbtwnz  10695  flid  10732  flqaddz  10745  flqdiv  10771  modqid  10799  frec2uzf1od  10856  iseqf1olemqk  10957  bcval5  11215  hashf1lem1  11299  eqs1  11410  pfxccatin12d  11531  abs2difabs  11889  fzomaxdiflem  11893  icodiamlt  11961  dfabsmax  11998  rexico  12002  mul0inf  12023  xrbdtri  12058  sumeq2  12141  sumsnf  12192  fsum00  12245  prodeq2  12340  prodsnf  12375  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitscmp  12741  gcd0id  12772  gcdneg  12775  nn0seqcvgd  12835  lcmval  12857  lcmneg  12868  qredeq  12890  prmind2  12914  pcpremul  13092  pcidlem  13122  pcgcd1  13127  fldivp1  13147  pcfaclem  13148  4sqlem17  13206  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemex  13354  ennnfonelemnn0  13362  mnd1  13811  grp1  13960  0subg  14051  nmznsg  14065  ghmpreima  14118  ghmeql  14119  ghmnsgpreima  14121  kerf1ghm  14126  ring1  14413  dvdsrmuld  14452  1unit  14463  unitmulcl  14469  unitgrp  14472  unitnegcl  14486  rhmdvdsr  14531  elrhmunit  14533  subrngintm  14569  subrguss  14593  subrgunit  14596  rhmeql  14607  rhmima  14608  lsslsp  14815  rnglidlrng  14884  issubassa  15062  issubassa2  15084  fczpsrbag  15105  psrbaglecl  15109  psrbagcon  15111  mplsubgfilemm  15138  mplsubgfilemcl  15139  mplsubgfileminv  15140  tgcl  15214  distop  15235  epttop  15240  neiss  15300  opnneissb  15305  ssnei2  15307  innei  15313  lmconst  15366  cnpnei  15369  cnptopco  15372  cnss1  15376  cnss2  15377  cncnpi  15378  cncnp  15380  cnconst2  15383  cnrest  15385  cnptopresti  15388  cnpdis  15392  lmtopcnp  15400  neitx  15418  tx1cn  15419  tx2cn  15420  txcnp  15421  txcnmpt  15423  txdis1cn  15428  psmetsym  15479  psmetres2  15483  isxmetd  15497  xmetsym  15518  xmetpsmet  15519  metrtri  15527  xblss2ps  15554  xblss2  15555  xblcntrps  15563  xblcntr  15564  bdxmet  15651  bdmet  15652  bdmopn  15654  xmetxp  15657  xmetxpbl  15658  rescncf  15731  cncfco  15741  mulcncflem  15757  mulcncf  15758  suplociccreex  15774  ivthinclemlopn  15786  ivthinclemuopn  15788  hovera  15797  hoverlt1  15799  cnplimcim  15817  cnplimclemr  15819  limccnpcntop  15825  limccnp2cntop  15827  limccoap  15828  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcn  15850  dvaddxxbr  15851  dvmulxxbr  15852  dvcoapbr  15857  dvcjbr  15858  dvrecap  15863  rpabscxpbnd  16095  dvdsppwf1o  16202  chtqub  16215  bposlem1  16230  bposlem2  16231  lgsdirprm  16272  lgseisenlem1  16308  lgseisenlem2  16309  lgseisenlem3  16310  lgsquadlem1  16315  2sqlem8  16361  uspgr2wlkeq2  16726  clwwlknccat  16783  clwwlknonex2lem2  16798  eupthres  16817  refeq  17192  apdifflemf  17214  ltlenmkv  17239