Theorem mpbir2and 945

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:  nnnninfeq2  7141  nqnq0pi  7451  genpassg  7539  addnqpr  7574  mulnqpr  7590  distrprg  7601  1idpr  7605  ltexpri  7626  recexprlemex  7650  aptipr  7654  cauappcvgprlemladd  7671  ltntri  8099  add20  8445  inelr  8555  recgt0  8821  prodgt0  8823  squeeze0  8875  suprzclex  9365  eluzadd  9570  eluzsub  9571  xrletrid  9819  xrre  9834  xrre3  9836  xleadd1a  9887  elioc2  9950  elico2  9951  elicc2  9952  elfz1eq  10049  fztri3or  10053  fznatpl1  10090  nn0fz0  10133  fzctr  10147  fzo1fzo0n0  10197  fzoaddel  10206  exbtwnz  10265  flid  10298  flqaddz  10311  flqdiv  10335  modqid  10363  frec2uzf1od  10420  iseqf1olemqk  10508  bcval5  10757  abs2difabs  11131  fzomaxdiflem  11135  icodiamlt  11203  dfabsmax  11240  rexico  11244  mul0inf  11263  xrbdtri  11298  sumeq2  11381  sumsnf  11431  fsum00  11484  prodeq2  11579  prodsnf  11614  zsupcllemstep  11960  zssinfcl  11963  gcd0id  11994  gcdneg  11997  nn0seqcvgd  12055  lcmval  12077  lcmneg  12088  qredeq  12110  prmind2  12134  pw2dvdseu  12182  hashdvds  12235  pcpremul  12307  pcidlem  12336  pcgcd1  12341  fldivp1  12360  pcfaclem  12361  ennnfonelemex  12429  ennnfonelemnn0  12437  mnd1  12869  grp1  13003  0subg  13091  nmznsg  13105  ring1  13309  dvdsrmuld  13344  1unit  13355  unitmulcl  13361  unitgrp  13364  unitnegcl  13378  subrngintm  13432  subrguss  13456  subrgunit  13459  lsslsp  13618  rnglidlrng  13687  tgcl  13860  distop  13881  epttop  13886  neiss  13946  opnneissb  13951  ssnei2  13953  innei  13959  lmconst  14012  cnpnei  14015  cnptopco  14018  cnss1  14022  cnss2  14023  cncnpi  14024  cncnp  14026  cnconst2  14029  cnrest  14031  cnptopresti  14034  cnpdis  14038  lmtopcnp  14046  neitx  14064  tx1cn  14065  tx2cn  14066  txcnp  14067  txcnmpt  14069  txdis1cn  14074  psmetsym  14125  psmetres2  14129  isxmetd  14143  xmetsym  14164  xmetpsmet  14165  metrtri  14173  xblss2ps  14200  xblss2  14201  xblcntrps  14209  xblcntr  14210  bdxmet  14297  bdmet  14298  bdmopn  14300  xmetxp  14303  xmetxpbl  14304  rescncf  14364  cncfco  14374  mulcncflem  14386  mulcncf  14387  suplociccreex  14398  ivthinclemlopn  14410  ivthinclemuopn  14412  cnplimcim  14432  cnplimclemr  14434  limccnpcntop  14440  limccnp2cntop  14442  limccoap  14443  dvidlemap  14456  dvcn  14460  dvaddxxbr  14461  dvmulxxbr  14462  dvcoapbr  14467  dvcjbr  14468  dvrecap  14473  rpabscxpbnd  14655  lgsdirprm  14731  lgseisenlem1  14746  lgseisenlem2  14747  2sqlem8  14766  refeq  15073  apdifflemf  15091  ltlenmkv  15115