Theorem mpbir2and 952

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  3779  nnnninfeq2  7328  nqnq0pi  7658  genpassg  7746  addnqpr  7781  mulnqpr  7797  distrprg  7808  1idpr  7812  ltexpri  7833  recexprlemex  7857  aptipr  7861  cauappcvgprlemladd  7878  ltntri  8307  add20  8654  inelr  8764  recgt0  9030  prodgt0  9032  squeeze0  9084  suprzclex  9578  eluzadd  9785  eluzsub  9786  xrletrid  10040  xrre  10055  xrre3  10057  xleadd1a  10108  elioc2  10171  elico2  10172  elicc2  10173  elfz1eq  10270  fztri3or  10274  fznatpl1  10311  nn0fz0  10354  fzctr  10368  fzo1fzo0n0  10423  fzoaddel  10433  elincfzoext  10439  zsupcllemstep  10490  zssinfcl  10493  exbtwnz  10511  flid  10545  flqaddz  10558  flqdiv  10584  modqid  10612  frec2uzf1od  10669  iseqf1olemqk  10770  bcval5  11026  eqs1  11206  pfxccatin12d  11327  abs2difabs  11670  fzomaxdiflem  11674  icodiamlt  11742  dfabsmax  11779  rexico  11783  mul0inf  11803  xrbdtri  11838  sumeq2  11921  sumsnf  11972  fsum00  12025  prodeq2  12120  prodsnf  12155  bitsfzolem  12517  bitsfzo  12518  bitsmod  12519  bitscmp  12521  gcd0id  12552  gcdneg  12555  nn0seqcvgd  12615  lcmval  12637  lcmneg  12648  qredeq  12670  prmind2  12694  pw2dvdseu  12742  hashdvds  12795  pcpremul  12868  pcidlem  12898  pcgcd1  12903  fldivp1  12923  pcfaclem  12924  4sqlem17  12982  ennnfonelemex  13037  ennnfonelemnn0  13045  mnd1  13540  grp1  13691  0subg  13788  nmznsg  13802  ghmpreima  13855  ghmeql  13856  ghmnsgpreima  13858  kerf1ghm  13863  ring1  14075  dvdsrmuld  14113  1unit  14124  unitmulcl  14130  unitgrp  14133  unitnegcl  14147  rhmdvdsr  14192  elrhmunit  14194  subrngintm  14229  subrguss  14253  subrgunit  14256  rhmeql  14267  rhmima  14268  lsslsp  14446  rnglidlrng  14515  fczpsrbag  14688  mplsubgfilemm  14715  mplsubgfilemcl  14716  mplsubgfileminv  14717  tgcl  14791  distop  14812  epttop  14817  neiss  14877  opnneissb  14882  ssnei2  14884  innei  14890  lmconst  14943  cnpnei  14946  cnptopco  14949  cnss1  14953  cnss2  14954  cncnpi  14955  cncnp  14957  cnconst2  14960  cnrest  14962  cnptopresti  14965  cnpdis  14969  lmtopcnp  14977  neitx  14995  tx1cn  14996  tx2cn  14997  txcnp  14998  txcnmpt  15000  txdis1cn  15005  psmetsym  15056  psmetres2  15060  isxmetd  15074  xmetsym  15095  xmetpsmet  15096  metrtri  15104  xblss2ps  15131  xblss2  15132  xblcntrps  15140  xblcntr  15141  bdxmet  15228  bdmet  15229  bdmopn  15231  xmetxp  15234  xmetxpbl  15235  rescncf  15308  cncfco  15318  mulcncflem  15334  mulcncf  15335  suplociccreex  15351  ivthinclemlopn  15363  ivthinclemuopn  15365  hovera  15374  hoverlt1  15376  cnplimcim  15394  cnplimclemr  15396  limccnpcntop  15402  limccnp2cntop  15404  limccoap  15405  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dvcn  15427  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  dvrecap  15440  rpabscxpbnd  15667  dvdsppwf1o  15716  lgsdirprm  15766  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgsquadlem1  15809  2sqlem8  15855  uspgr2wlkeq2  16220  clwwlknccat  16277  clwwlknonex2lem2  16292  eupthres  16311  refeq  16653  apdifflemf  16671  ltlenmkv  16695