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  isfsuppfid  7297  nnnninfeq2  7475  nqnq0pi  7811  genpassg  7899  addnqpr  7934  mulnqpr  7950  distrprg  7961  1idpr  7965  ltexpri  7986  recexprlemex  8010  aptipr  8014  cauappcvgprlemladd  8031  letrid  8449  ltntri  8461  add20  8809  inelr  8920  recgt0  9188  prodgt0  9190  squeeze0  9242  suprzclex  9754  eluzadd  9966  eluzsub  9967  xrletrid  10223  xrre  10238  xrre3  10240  xleadd1a  10291  elioc2  10354  elico2  10355  elicc2  10356  elfz1eq  10455  fztri3or  10459  fzspl  10492  fznatpl1  10499  nn0fz0  10542  fzctr  10556  fzo1fzo0n0  10611  fzoaddel  10621  elincfzoext  10627  zsupcllemstep  10678  zssinfcl  10681  exbtwnz  10701  flid  10739  flqaddz  10752  flqdiv  10778  modqid  10806  frec2uzf1od  10863  iseqf1olemqk  10964  bcval5  11222  hashf1lem1  11306  eqs1  11417  pfxccatin12d  11538  abs2difabs  11896  fzomaxdiflem  11900  icodiamlt  11968  dfabsmax  12005  rexico  12009  mul0inf  12031  xrbdtri  12066  sumeq2  12149  sumsnf  12200  fsum00  12253  prodeq2  12348  prodsnf  12383  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitscmp  12749  gcd0id  12780  gcdneg  12783  nn0seqcvgd  12843  lcmval  12865  lcmneg  12876  qredeq  12898  prmind2  12922  pcpremul  13100  pcidlem  13130  pcgcd1  13135  fldivp1  13155  pcfaclem  13156  4sqlem17  13214  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemex  13362  ennnfonelemnn0  13370  mnd1  13820  grp1  13969  0subg  14060  nmznsg  14074  ghmpreima  14127  ghmeql  14128  ghmnsgpreima  14130  kerf1ghm  14135  cntzsgrpcl  14166  cntzsubm  14169  cntzsubg  14170  cntzmhm  14172  ring1  14470  dvdsrmuld  14511  1unit  14522  unitmulcl  14528  unitgrp  14531  unitnegcl  14545  rhmdvdsr  14590  elrhmunit  14592  subrngintm  14628  subrguss  14652  subrgunit  14655  rhmeql  14666  rhmima  14667  lsslsp  14874  rnglidlrng  14943  issubassa  15121  issubassa2  15143  fczpsrbag  15169  psrbaglecl  15172  psrbagcon  15174  tgcl  15307  distop  15328  epttop  15333  neiss  15393  opnneissb  15398  ssnei2  15400  innei  15406  lmconst  15459  cnpnei  15462  cnptopco  15465  cnss1  15469  cnss2  15470  cncnpi  15471  cncnp  15473  cnconst2  15476  cnrest  15478  cnptopresti  15481  cnpdis  15485  lmtopcnp  15493  neitx  15511  tx1cn  15512  tx2cn  15513  txcnp  15514  txcnmpt  15516  txdis1cn  15521  psmetsym  15572  psmetres2  15576  isxmetd  15590  xmetsym  15611  xmetpsmet  15612  metrtri  15620  xblss2ps  15647  xblss2  15648  xblcntrps  15656  xblcntr  15657  bdxmet  15744  bdmet  15745  bdmopn  15747  xmetxp  15750  xmetxpbl  15751  rescncf  15824  cncfco  15834  mulcncflem  15850  mulcncf  15851  suplociccreex  15867  ivthinclemlopn  15879  ivthinclemuopn  15881  hovera  15890  hoverlt1  15892  cnplimcim  15910  cnplimclemr  15912  limccnpcntop  15918  limccnp2cntop  15920  limccoap  15921  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcn  15943  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  rpabscxpbnd  16192  dvdsppwf1o  16300  chtqub  16313  bposlem1  16328  bposlem2  16329  lgsdirprm  16375  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgsquadlem1  16418  2sqlem8  16464  uspgr2wlkeq2  16829  clwwlknccat  16886  clwwlknonex2lem2  16901  eupthres  16920  refeq  17296  apdifflemf  17319  ltlenmkv  17344