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  9903  ixxss2  9904  ixxss12  9905  ubioc1  9928  lbico1  9929  lbicc2  9983  ubicc2  9984  elicod  10264  modqelico  10333  zmodfz  10345  modqmuladdim  10366  addmodid  10371  phicl2  12213  isstruct2r  12472  issubmd  12864  mndissubm  12865  submid  12867  0subm  12870  mhmima  12874  mhmeql  12875  issubgrpd2  13048  grpissubg  13052  subgintm  13056  nmzsubg  13068  eqger  13081  eqgcpbl  13085  unitsubm  13286  subrgsubm  13353  subrgugrp  13359  subrgintm  13362  lmtopcnp  13720  xmeter  13906  tgqioo  14017  suplociccreex  14072  dedekindicc  14081  ivthinclemlopn  14084  ivthinclemuopn  14086  sin0pilem2  14173  pilem3  14174  coseq0q4123  14225