Theorem mpbir3and 1183

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

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

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 983

This theorem is referenced by:  ixxss1  10033  ixxss2  10034  ixxss12  10035  ubioc1  10058  lbico1  10059  lbicc2  10113  ubicc2  10114  elicod  10414  modqelico  10486  zmodfz  10498  modqmuladdim  10519  addmodid  10524  phicl2  12580  4sqlem12  12769  isstruct2r  12887  issubmd  13350  mndissubm  13351  submid  13353  subsubm  13359  0subm  13360  mhmima  13367  mhmeql  13368  issubgrpd2  13570  grpissubg  13574  subgintm  13578  nmzsubg  13590  eqger  13604  eqgcpbl  13608  ghmrn  13637  ghmpreima  13646  unitsubm  13925  subrgsubm  14040  subrgugrp  14046  subrgintm  14049  islssmd  14165  lsssubg  14183  islss4  14188  issubrgd  14258  lidlsubg  14292  2idlcpblrng  14329  mplsubgfi  14507  lmtopcnp  14766  xmeter  14952  tgqioo  15071  suplociccreex  15140  dedekindicc  15149  ivthinclemlopn  15152  ivthinclemuopn  15154  sin0pilem2  15298  pilem3  15299  coseq0q4123  15350