Theorem mpbir2and 929

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 304	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
4		mpbir2and.3	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
5	3, 4	mpbird 166	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nqnq0pi  7270  genpassg  7358  addnqpr  7393  mulnqpr  7409  distrprg  7420  1idpr  7424  ltexpri  7445  recexprlemex  7469  aptipr  7473  cauappcvgprlemladd  7490  ltntri  7914  add20  8260  inelr  8370  recgt0  8632  prodgt0  8634  squeeze0  8686  suprzclex  9173  eluzadd  9378  eluzsub  9379  xrre  9633  xrre3  9635  xleadd1a  9686  elioc2  9749  elico2  9750  elicc2  9751  elfz1eq  9846  fztri3or  9850  fznatpl1  9887  nn0fz0  9930  fzctr  9941  fzo1fzo0n0  9991  fzoaddel  10000  exbtwnz  10059  flid  10088  flqaddz  10101  flqdiv  10125  modqid  10153  frec2uzf1od  10210  iseqf1olemqk  10298  bcval5  10541  abs2difabs  10912  fzomaxdiflem  10916  icodiamlt  10984  dfabsmax  11021  rexico  11025  mul0inf  11044  xrbdtri  11077  sumeq2  11160  sumsnf  11210  fsum00  11263  prodeq2  11358  zsupcllemstep  11674  zssinfcl  11677  gcd0id  11703  gcdneg  11706  nn0seqcvgd  11758  lcmval  11780  lcmneg  11791  qredeq  11813  prmind2  11837  pw2dvdseu  11882  hashdvds  11933  ennnfonelemex  11963  ennnfonelemnn0  11971  tgcl  12272  distop  12293  epttop  12298  neiss  12358  opnneissb  12363  ssnei2  12365  innei  12371  lmconst  12424  cnpnei  12427  cnptopco  12430  cnss1  12434  cnss2  12435  cncnpi  12436  cncnp  12438  cnconst2  12441  cnrest  12443  cnptopresti  12446  cnpdis  12450  lmtopcnp  12458  neitx  12476  tx1cn  12477  tx2cn  12478  txcnp  12479  txcnmpt  12481  txdis1cn  12486  psmetsym  12537  psmetres2  12541  isxmetd  12555  xmetsym  12576  xmetpsmet  12577  metrtri  12585  xblss2ps  12612  xblss2  12613  xblcntrps  12621  xblcntr  12622  bdxmet  12709  bdmet  12710  bdmopn  12712  xmetxp  12715  xmetxpbl  12716  rescncf  12776  cncfco  12786  mulcncflem  12798  mulcncf  12799  suplociccreex  12810  ivthinclemlopn  12822  ivthinclemuopn  12824  cnplimcim  12844  cnplimclemr  12846  limccnpcntop  12852  limccnp2cntop  12854  limccoap  12855  dvidlemap  12868  dvcn  12872  dvaddxxbr  12873  dvmulxxbr  12874  dvcoapbr  12879  dvcjbr  12880  dvrecap  12885  rpabscxpbnd  13067  refeq  13398  apdifflemf  13414