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  9680  ixxss2  9681  ixxss12  9682  ubioc1  9705  lbico1  9706  lbicc2  9760  ubicc2  9761  modqelico  10100  zmodfz  10112  modqmuladdim  10133  addmodid  10138  phicl2  11879  isstruct2r  11959  lmtopcnp  12408  xmeter  12594  tgqioo  12705  suplociccreex  12760  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemuopn  12774  sin0pilem2  12852  pilem3  12853  coseq0q4123  12904