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  3780  nnnninfeq2  7333  nqnq0pi  7663  genpassg  7751  addnqpr  7786  mulnqpr  7802  distrprg  7813  1idpr  7817  ltexpri  7838  recexprlemex  7862  aptipr  7866  cauappcvgprlemladd  7883  ltntri  8312  add20  8659  inelr  8769  recgt0  9035  prodgt0  9037  squeeze0  9089  suprzclex  9583  eluzadd  9790  eluzsub  9791  xrletrid  10045  xrre  10060  xrre3  10062  xleadd1a  10113  elioc2  10176  elico2  10177  elicc2  10178  elfz1eq  10275  fztri3or  10279  fznatpl1  10316  nn0fz0  10359  fzctr  10373  fzo1fzo0n0  10428  fzoaddel  10438  elincfzoext  10444  zsupcllemstep  10495  zssinfcl  10498  exbtwnz  10516  flid  10550  flqaddz  10563  flqdiv  10589  modqid  10617  frec2uzf1od  10674  iseqf1olemqk  10775  bcval5  11031  eqs1  11214  pfxccatin12d  11335  abs2difabs  11691  fzomaxdiflem  11695  icodiamlt  11763  dfabsmax  11800  rexico  11804  mul0inf  11824  xrbdtri  11859  sumeq2  11942  sumsnf  11993  fsum00  12046  prodeq2  12141  prodsnf  12176  bitsfzolem  12538  bitsfzo  12539  bitsmod  12540  bitscmp  12542  gcd0id  12573  gcdneg  12576  nn0seqcvgd  12636  lcmval  12658  lcmneg  12669  qredeq  12691  prmind2  12715  pw2dvdseu  12763  hashdvds  12816  pcpremul  12889  pcidlem  12919  pcgcd1  12924  fldivp1  12944  pcfaclem  12945  4sqlem17  13003  ennnfonelemex  13058  ennnfonelemnn0  13066  mnd1  13561  grp1  13712  0subg  13809  nmznsg  13823  ghmpreima  13876  ghmeql  13877  ghmnsgpreima  13879  kerf1ghm  13884  ring1  14096  dvdsrmuld  14134  1unit  14145  unitmulcl  14151  unitgrp  14154  unitnegcl  14168  rhmdvdsr  14213  elrhmunit  14215  subrngintm  14250  subrguss  14274  subrgunit  14277  rhmeql  14288  rhmima  14289  lsslsp  14467  rnglidlrng  14536  fczpsrbag  14709  psrbaglecl  14713  psrbagcon  14714  mplsubgfilemm  14741  mplsubgfilemcl  14742  mplsubgfileminv  14743  tgcl  14817  distop  14838  epttop  14843  neiss  14903  opnneissb  14908  ssnei2  14910  innei  14916  lmconst  14969  cnpnei  14972  cnptopco  14975  cnss1  14979  cnss2  14980  cncnpi  14981  cncnp  14983  cnconst2  14986  cnrest  14988  cnptopresti  14991  cnpdis  14995  lmtopcnp  15003  neitx  15021  tx1cn  15022  tx2cn  15023  txcnp  15024  txcnmpt  15026  txdis1cn  15031  psmetsym  15082  psmetres2  15086  isxmetd  15100  xmetsym  15121  xmetpsmet  15122  metrtri  15130  xblss2ps  15157  xblss2  15158  xblcntrps  15166  xblcntr  15167  bdxmet  15254  bdmet  15255  bdmopn  15257  xmetxp  15260  xmetxpbl  15261  rescncf  15334  cncfco  15344  mulcncflem  15360  mulcncf  15361  suplociccreex  15377  ivthinclemlopn  15389  ivthinclemuopn  15391  hovera  15400  hoverlt1  15402  cnplimcim  15420  cnplimclemr  15422  limccnpcntop  15428  limccnp2cntop  15430  limccoap  15431  dvidlemap  15444  dvidrelem  15445  dvidsslem  15446  dvcn  15453  dvaddxxbr  15454  dvmulxxbr  15455  dvcoapbr  15460  dvcjbr  15461  dvrecap  15466  rpabscxpbnd  15693  dvdsppwf1o  15742  lgsdirprm  15792  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgsquadlem1  15835  2sqlem8  15881  uspgr2wlkeq2  16246  clwwlknccat  16303  clwwlknonex2lem2  16318  eupthres  16337  refeq  16695  apdifflemf  16717  ltlenmkv  16742