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  10243  ixxss2  10244  ixxss12  10245  ubioc1  10268  lbico1  10269  lbicc2  10323  ubicc2  10324  lincmble  10343  elicod  10631  modqelico  10703  zmodfz  10715  modqmuladdim  10736  addmodid  10741  phicl2  12919  4sqlem12  13108  isstruct2r  13244  issubmd  13708  mndissubm  13709  submid  13711  subsubm  13717  0subm  13718  mhmima  13725  mhmeql  13726  issubgrpd2  13928  grpissubg  13932  subgintm  13936  nmzsubg  13948  eqger  13962  eqgcpbl  13966  ghmrn  13995  ghmpreima  14004  unitsubm  14286  subrgsubm  14402  subrgugrp  14408  subrgintm  14411  islssmd  14556  lsssubg  14574  islss4  14579  issubrgd  14649  lidlsubg  14683  2idlcpblrng  14720  mplsubgfi  14905  lmtopcnp  15164  xmeter  15350  tgqioo  15469  suplociccreex  15538  dedekindicc  15547  ivthinclemlopn  15550  ivthinclemuopn  15552  sin0pilem2  15696  pilem3  15697  coseq0q4123  15748  uhgrissubgr  16305  egrsubgr  16307  uhgrspansubgr  16321  wlkres  16423