Theorem mpbir3and 1165

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 1162	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏))
5		mpbir3and.4	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))
6	4, 5	mpbird 166	1 ⊢ (𝜑 → 𝜓)

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

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 965

This theorem is referenced by:  ixxss1  9717  ixxss2  9718  ixxss12  9719  ubioc1  9742  lbico1  9743  lbicc2  9797  ubicc2  9798  modqelico  10138  zmodfz  10150  modqmuladdim  10171  addmodid  10176  phicl2  11926  isstruct2r  12009  lmtopcnp  12458  xmeter  12644  tgqioo  12755  suplociccreex  12810  dedekindicc  12819  ivthinclemlopn  12822  ivthinclemuopn  12824  sin0pilem2  12911  pilem3  12912  coseq0q4123  12963