Theorem mpbir2and 928

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  7246  genpassg  7334  addnqpr  7369  mulnqpr  7385  distrprg  7396  1idpr  7400  ltexpri  7421  recexprlemex  7445  aptipr  7449  cauappcvgprlemladd  7466  ltntri  7890  add20  8236  inelr  8346  recgt0  8608  prodgt0  8610  squeeze0  8662  suprzclex  9149  eluzadd  9354  eluzsub  9355  xrre  9603  xrre3  9605  xleadd1a  9656  elioc2  9719  elico2  9720  elicc2  9721  elfz1eq  9815  fztri3or  9819  fznatpl1  9856  nn0fz0  9899  fzctr  9910  fzo1fzo0n0  9960  fzoaddel  9969  exbtwnz  10028  flid  10057  flqaddz  10070  flqdiv  10094  modqid  10122  frec2uzf1od  10179  iseqf1olemqk  10267  bcval5  10509  abs2difabs  10880  fzomaxdiflem  10884  icodiamlt  10952  dfabsmax  10989  rexico  10993  mul0inf  11012  xrbdtri  11045  sumeq2  11128  sumsnf  11178  fsum00  11231  prodeq2  11326  zsupcllemstep  11638  zssinfcl  11641  gcd0id  11667  gcdneg  11670  nn0seqcvgd  11722  lcmval  11744  lcmneg  11755  qredeq  11777  prmind2  11801  pw2dvdseu  11846  hashdvds  11897  ennnfonelemex  11927  ennnfonelemnn0  11935  tgcl  12233  distop  12254  epttop  12259  neiss  12319  opnneissb  12324  ssnei2  12326  innei  12332  lmconst  12385  cnpnei  12388  cnptopco  12391  cnss1  12395  cnss2  12396  cncnpi  12397  cncnp  12399  cnconst2  12402  cnrest  12404  cnptopresti  12407  cnpdis  12411  lmtopcnp  12419  neitx  12437  tx1cn  12438  tx2cn  12439  txcnp  12440  txcnmpt  12442  txdis1cn  12447  psmetsym  12498  psmetres2  12502  isxmetd  12516  xmetsym  12537  xmetpsmet  12538  metrtri  12546  xblss2ps  12573  xblss2  12574  xblcntrps  12582  xblcntr  12583  bdxmet  12670  bdmet  12671  bdmopn  12673  xmetxp  12676  xmetxpbl  12677  rescncf  12737  cncfco  12747  mulcncflem  12759  mulcncf  12760  suplociccreex  12771  ivthinclemlopn  12783  ivthinclemuopn  12785  cnplimcim  12805  cnplimclemr  12807  limccnpcntop  12813  limccnp2cntop  12815  limccoap  12816  dvidlemap  12829  dvcn  12833  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846  refeq  13223