Theorem mpbir3and 1164

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
mpbir3and.1	⊢ (𝜑 → 𝜒)
mpbir3and.2	⊢ (𝜑 → 𝜃)
mpbir3and.3	⊢ (𝜑 → 𝜏)
mpbir3and.4	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Assertion

Ref	Expression
mpbir3and	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbir3and

Step	Hyp	Ref	Expression
1		mpbir3and.1	. . 3 ⊢ (𝜑 → 𝜒)
2		mpbir3and.2	. . 3 ⊢ (𝜑 → 𝜃)
3		mpbir3and.3	. . 3 ⊢ (𝜑 → 𝜏)
4	1, 2, 3	3jca 1161	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
5		mpbir3and.4	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
6	4, 5	mpbird 166	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104   ∧ w3a 962

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  df-3an 964

This theorem is referenced by:  ixxss1  9687  ixxss2  9688  ixxss12  9689  ubioc1  9712  lbico1  9713  lbicc2  9767  ubicc2  9768  modqelico  10107  zmodfz  10119  modqmuladdim  10140  addmodid  10145  phicl2  11890  isstruct2r  11970  lmtopcnp  12419  xmeter  12605  tgqioo  12716  suplociccreex  12771  dedekindicc  12780  ivthinclemlopn  12783  ivthinclemuopn  12785  sin0pilem2  12863  pilem3  12864  coseq0q4123  12915