Theorem mpbir2and 891

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 301	. 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nqnq0pi  7051  genpassg  7139  addnqpr  7174  mulnqpr  7190  distrprg  7201  1idpr  7205  ltexpri  7226  recexprlemex  7250  aptipr  7254  cauappcvgprlemladd  7271  add20  8006  inelr  8115  recgt0  8365  prodgt0  8367  squeeze0  8419  suprzclex  8898  eluzadd  9101  eluzsub  9102  xrre  9336  xrre3  9338  elioc2  9408  elico2  9409  elicc2  9410  elfz1eq  9503  fztri3or  9507  fznatpl1  9544  nn0fz0  9587  fzctr  9598  fzo1fzo0n0  9648  fzoaddel  9657  exbtwnz  9716  flid  9745  flqaddz  9758  flqdiv  9782  modqid  9810  frec2uzf1od  9867  iseqf1olemqk  9977  ibcval5  10225  abs2difabs  10595  fzomaxdiflem  10599  icodiamlt  10667  dfabsmax  10704  rexico  10708  sumeq2  10802  sumsnf  10857  fsum00  10910  zsupcllemstep  11273  zssinfcl  11276  gcd0id  11302  gcdneg  11305  nn0seqcvgd  11355  lcmval  11377  lcmneg  11388  qredeq  11410  prmind2  11434  pw2dvdseu  11478  hashdvds  11529  tgcl  11818  distop  11839  epttop  11844  rescncf  11903  cncfco  11913