Theorem mpbi2and 884

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
mpbi2and.1	⊢ (𝜑 → 𝜓)
mpbi2and.2	⊢ (𝜑 → 𝜒)
mpbi2and.3	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))

Assertion

Ref	Expression
mpbi2and	⊢ (𝜑 → 𝜃)

Proof of Theorem mpbi2and

Step	Hyp	Ref	Expression
1		mpbi2and.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpbi2and.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 300	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		mpbi2and.3	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))
5	3, 4	mpbid 145	1 ⊢ (𝜑 → 𝜃)

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  supisoti  6423  remim  9747  resqrtcl  9915  divalgmod  10327  oddpwdclemxy  10547