Theorem mpbir3and 1180

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

Syntax hints:   → wi 4   ↔ wb 105   ∧ w3a 978

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

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  ixxss1  9906  ixxss2  9907  ixxss12  9908  ubioc1  9931  lbico1  9932  lbicc2  9986  ubicc2  9987  elicod  10267  modqelico  10336  zmodfz  10348  modqmuladdim  10369  addmodid  10374  phicl2  12216  isstruct2r  12475  issubmd  12870  mndissubm  12871  submid  12873  0subm  12876  mhmima  12880  mhmeql  12881  issubgrpd2  13055  grpissubg  13059  subgintm  13063  nmzsubg  13075  eqger  13088  eqgcpbl  13092  unitsubm  13293  subrgsubm  13360  subrgugrp  13366  subrgintm  13369  islssmd  13451  lsssubg  13469  islss4  13474  lmtopcnp  13789  xmeter  13975  tgqioo  14086  suplociccreex  14141  dedekindicc  14150  ivthinclemlopn  14153  ivthinclemuopn  14155  sin0pilem2  14242  pilem3  14243  coseq0q4123  14294