Theorem mpbir3and 1185

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

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

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 985

This theorem is referenced by:  ixxss1  10068  ixxss2  10069  ixxss12  10070  ubioc1  10093  lbico1  10094  lbicc2  10148  ubicc2  10149  elicod  10451  modqelico  10523  zmodfz  10535  modqmuladdim  10556  addmodid  10561  phicl2  12702  4sqlem12  12891  isstruct2r  13009  issubmd  13473  mndissubm  13474  submid  13476  subsubm  13482  0subm  13483  mhmima  13490  mhmeql  13491  issubgrpd2  13693  grpissubg  13697  subgintm  13701  nmzsubg  13713  eqger  13727  eqgcpbl  13731  ghmrn  13760  ghmpreima  13769  unitsubm  14048  subrgsubm  14163  subrgugrp  14169  subrgintm  14172  islssmd  14288  lsssubg  14306  islss4  14311  issubrgd  14381  lidlsubg  14415  2idlcpblrng  14452  mplsubgfi  14630  lmtopcnp  14889  xmeter  15075  tgqioo  15194  suplociccreex  15263  dedekindicc  15272  ivthinclemlopn  15275  ivthinclemuopn  15277  sin0pilem2  15421  pilem3  15422  coseq0q4123  15473