Theorem mpbir3and 1207

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

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

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 1007

This theorem is referenced by:  ixxss1  10259  ixxss2  10260  ixxss12  10261  ubioc1  10284  lbico1  10285  lbicc2  10339  ubicc2  10340  lincmble  10359  elicod  10651  modqelico  10723  zmodfz  10735  modqmuladdim  10756  addmodid  10761  phicl2  12939  4sqlem12  13128  isstruct2r  13310  issubmd  13732  mndissubm  13733  submid  13735  subsubm  13741  0subm  13742  mhmima  13749  mhmeql  13750  issubgrpd2  13946  grpissubg  13950  subgintm  13954  nmzsubg  13966  eqger  13980  eqgcpbl  13984  ghmrn  14013  ghmpreima  14022  unitsubm  14367  subrgsubm  14483  subrgugrp  14489  subrgintm  14492  islssmd  14636  lsssubg  14654  islss4  14659  issubrgd  14729  lidlsubg  14763  2idlcpblrng  14800  mplsubgfi  14985  lmtopcnp  15244  xmeter  15430  tgqioo  15549  suplociccreex  15618  dedekindicc  15627  ivthinclemlopn  15630  ivthinclemuopn  15632  sin0pilem2  15776  pilem3  15777  coseq0q4123  15828  uhgrissubgr  16385  egrsubgr  16387  uhgrspansubgr  16401  wlkres  16503