Theorem mpbir2and 953

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  3804  isfsuppd  7256  nnnninfeq2  7433  nqnq0pi  7769  genpassg  7857  addnqpr  7892  mulnqpr  7908  distrprg  7919  1idpr  7923  ltexpri  7944  recexprlemex  7968  aptipr  7972  cauappcvgprlemladd  7989  letrid  8406  ltntri  8418  add20  8766  inelr  8876  recgt0  9144  prodgt0  9146  squeeze0  9198  suprzclex  9697  eluzadd  9904  eluzsub  9905  xrletrid  10160  xrre  10175  xrre3  10177  xleadd1a  10228  elioc2  10291  elico2  10292  elicc2  10293  elfz1eq  10392  fztri3or  10396  fzspl  10428  fznatpl1  10435  nn0fz0  10478  fzctr  10492  fzo1fzo0n0  10547  fzoaddel  10557  elincfzoext  10563  zsupcllemstep  10614  zssinfcl  10617  exbtwnz  10637  flid  10671  flqaddz  10684  flqdiv  10710  modqid  10738  frec2uzf1od  10795  iseqf1olemqk  10896  bcval5  11153  eqs1  11344  pfxccatin12d  11465  abs2difabs  11821  fzomaxdiflem  11825  icodiamlt  11893  dfabsmax  11930  rexico  11934  mul0inf  11954  xrbdtri  11989  sumeq2  12072  sumsnf  12123  fsum00  12176  prodeq2  12271  prodsnf  12306  bitsfzolem  12668  bitsfzo  12669  bitsmod  12670  bitscmp  12672  gcd0id  12703  gcdneg  12706  nn0seqcvgd  12766  lcmval  12788  lcmneg  12799  qredeq  12821  prmind2  12845  pw2dvdseu  12893  pcpremul  13019  pcidlem  13049  pcgcd1  13054  fldivp1  13074  pcfaclem  13075  4sqlem17  13133  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemex  13252  ennnfonelemnn0  13260  mnd1  13713  grp1  13864  0subg  13955  nmznsg  13969  ghmpreima  14022  ghmeql  14023  ghmnsgpreima  14025  kerf1ghm  14030  ring1  14305  dvdsrmuld  14344  1unit  14355  unitmulcl  14361  unitgrp  14364  unitnegcl  14378  rhmdvdsr  14423  elrhmunit  14425  subrngintm  14461  subrguss  14485  subrgunit  14488  rhmeql  14499  rhmima  14500  lsslsp  14706  rnglidlrng  14775  fczpsrbag  14949  psrbaglecl  14953  psrbagcon  14955  mplsubgfilemm  14982  mplsubgfilemcl  14983  mplsubgfileminv  14984  tgcl  15058  distop  15079  epttop  15084  neiss  15144  opnneissb  15149  ssnei2  15151  innei  15157  lmconst  15210  cnpnei  15213  cnptopco  15216  cnss1  15220  cnss2  15221  cncnpi  15222  cncnp  15224  cnconst2  15227  cnrest  15229  cnptopresti  15232  cnpdis  15236  lmtopcnp  15244  neitx  15262  tx1cn  15263  tx2cn  15264  txcnp  15265  txcnmpt  15267  txdis1cn  15272  psmetsym  15323  psmetres2  15327  isxmetd  15341  xmetsym  15362  xmetpsmet  15363  metrtri  15371  xblss2ps  15398  xblss2  15399  xblcntrps  15407  xblcntr  15408  bdxmet  15495  bdmet  15496  bdmopn  15498  xmetxp  15501  xmetxpbl  15502  rescncf  15575  cncfco  15585  mulcncflem  15601  mulcncf  15602  suplociccreex  15618  ivthinclemlopn  15630  ivthinclemuopn  15632  hovera  15641  hoverlt1  15643  cnplimcim  15661  cnplimclemr  15663  limccnpcntop  15669  limccnp2cntop  15671  limccoap  15672  dvidlemap  15685  dvidrelem  15686  dvidsslem  15687  dvcn  15694  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  dvrecap  15707  rpabscxpbnd  15934  dvdsppwf1o  15986  lgsdirprm  16036  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem3  16074  lgsquadlem1  16079  2sqlem8  16125  uspgr2wlkeq2  16490  clwwlknccat  16547  clwwlknonex2lem2  16562  eupthres  16581  refeq  16947  apdifflemf  16969  ltlenmkv  16995