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  8442  ltntri  8454  add20  8802  inelr  8913  recgt0  9181  prodgt0  9183  squeeze0  9235  suprzclex  9746  eluzadd  9953  eluzsub  9954  xrletrid  10209  xrre  10224  xrre3  10226  xleadd1a  10277  elioc2  10340  elico2  10341  elicc2  10342  elfz1eq  10441  fztri3or  10445  fzspl  10478  fznatpl1  10485  nn0fz0  10528  fzctr  10542  fzo1fzo0n0  10597  fzoaddel  10607  elincfzoext  10613  zsupcllemstep  10664  zssinfcl  10667  exbtwnz  10687  flid  10721  flqaddz  10734  flqdiv  10760  modqid  10788  frec2uzf1od  10845  iseqf1olemqk  10946  bcval5  11203  hashf1lem1  11287  eqs1  11398  pfxccatin12d  11519  abs2difabs  11876  fzomaxdiflem  11880  icodiamlt  11948  dfabsmax  11985  rexico  11989  mul0inf  12009  xrbdtri  12044  sumeq2  12127  sumsnf  12178  fsum00  12231  prodeq2  12326  prodsnf  12361  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitscmp  12727  gcd0id  12758  gcdneg  12761  nn0seqcvgd  12821  lcmval  12843  lcmneg  12854  qredeq  12876  prmind2  12900  pw2dvdseu  12948  pcpremul  13074  pcidlem  13104  pcgcd1  13109  fldivp1  13129  pcfaclem  13130  4sqlem17  13188  ballotfilemfc0  13234  ballotfilemfcc  13235  ennnfonelemex  13307  ennnfonelemnn0  13315  mnd1  13764  grp1  13913  0subg  14004  nmznsg  14018  ghmpreima  14071  ghmeql  14072  ghmnsgpreima  14074  kerf1ghm  14079  ring1  14366  dvdsrmuld  14405  1unit  14416  unitmulcl  14422  unitgrp  14425  unitnegcl  14439  rhmdvdsr  14484  elrhmunit  14486  subrngintm  14522  subrguss  14546  subrgunit  14549  rhmeql  14560  rhmima  14561  lsslsp  14768  rnglidlrng  14837  issubassa  15015  issubassa2  15037  fczpsrbag  15058  psrbaglecl  15062  psrbagcon  15064  mplsubgfilemm  15091  mplsubgfilemcl  15092  mplsubgfileminv  15093  tgcl  15167  distop  15188  epttop  15193  neiss  15253  opnneissb  15258  ssnei2  15260  innei  15266  lmconst  15319  cnpnei  15322  cnptopco  15325  cnss1  15329  cnss2  15330  cncnpi  15331  cncnp  15333  cnconst2  15336  cnrest  15338  cnptopresti  15341  cnpdis  15345  lmtopcnp  15353  neitx  15371  tx1cn  15372  tx2cn  15373  txcnp  15374  txcnmpt  15376  txdis1cn  15381  psmetsym  15432  psmetres2  15436  isxmetd  15450  xmetsym  15471  xmetpsmet  15472  metrtri  15480  xblss2ps  15507  xblss2  15508  xblcntrps  15516  xblcntr  15517  bdxmet  15604  bdmet  15605  bdmopn  15607  xmetxp  15610  xmetxpbl  15611  rescncf  15684  cncfco  15694  mulcncflem  15710  mulcncf  15711  suplociccreex  15727  ivthinclemlopn  15739  ivthinclemuopn  15741  hovera  15750  hoverlt1  15752  cnplimcim  15770  cnplimclemr  15772  limccnpcntop  15778  limccnp2cntop  15780  limccoap  15781  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvcn  15803  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcjbr  15811  dvrecap  15816  rpabscxpbnd  16048  dvdsppwf1o  16109  lgsdirprm  16165  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgsquadlem1  16208  2sqlem8  16254  uspgr2wlkeq2  16619  clwwlknccat  16676  clwwlknonex2lem2  16691  eupthres  16710  refeq  17085  apdifflemf  17107  ltlenmkv  17132