Theorem mpbir3and 1204

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

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

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 1004

This theorem is referenced by:  ixxss1  10108  ixxss2  10109  ixxss12  10110  ubioc1  10133  lbico1  10134  lbicc2  10188  ubicc2  10189  elicod  10492  modqelico  10564  zmodfz  10576  modqmuladdim  10597  addmodid  10602  phicl2  12744  4sqlem12  12933  isstruct2r  13051  issubmd  13515  mndissubm  13516  submid  13518  subsubm  13524  0subm  13525  mhmima  13532  mhmeql  13533  issubgrpd2  13735  grpissubg  13739  subgintm  13743  nmzsubg  13755  eqger  13769  eqgcpbl  13773  ghmrn  13802  ghmpreima  13811  unitsubm  14091  subrgsubm  14206  subrgugrp  14212  subrgintm  14215  islssmd  14331  lsssubg  14349  islss4  14354  issubrgd  14424  lidlsubg  14458  2idlcpblrng  14495  mplsubgfi  14673  lmtopcnp  14932  xmeter  15118  tgqioo  15237  suplociccreex  15306  dedekindicc  15315  ivthinclemlopn  15318  ivthinclemuopn  15320  sin0pilem2  15464  pilem3  15465  coseq0q4123  15516  wlkres  16098