Theorem mpbir2and 851

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

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nqnq0pi  6536  genpassg  6624  addnqpr  6659  mulnqpr  6675  distrprg  6686  1idpr  6690  ltexpri  6711  recexprlemex  6735  aptipr  6739  cauappcvgprlemladd  6756  add20  7469  inelr  7575  recgt0  7816  prodgt0  7818  squeeze0  7870  eluzadd  8501  eluzsub  8502  xrre  8733  xrre3  8735  elioc2  8805  elico2  8806  elicc2  8807  elfz1eq  8899  fztri3or  8903  fznatpl1  8938  nn0fz0  8978  fzctr  8991  fzo1fzo0n0  9039  fzoaddel  9048  qbtwnz  9106  flid  9126  flqaddz  9139  flqdiv  9163  frec2uzf1od  9192  expival  9257  abs2difabs  9704  fzomaxdiflem  9708  icodiamlt  9776  nn0seqcvgd  9880