Theorem mpbir3and 1206

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

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

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 1006

This theorem is referenced by:  ixxss1  10144  ixxss2  10145  ixxss12  10146  ubioc1  10169  lbico1  10170  lbicc2  10224  ubicc2  10225  elicod  10530  modqelico  10602  zmodfz  10614  modqmuladdim  10635  addmodid  10640  phicl2  12809  4sqlem12  12998  isstruct2r  13116  issubmd  13580  mndissubm  13581  submid  13583  subsubm  13589  0subm  13590  mhmima  13597  mhmeql  13598  issubgrpd2  13800  grpissubg  13804  subgintm  13808  nmzsubg  13820  eqger  13834  eqgcpbl  13838  ghmrn  13867  ghmpreima  13876  unitsubm  14157  subrgsubm  14272  subrgugrp  14278  subrgintm  14281  islssmd  14397  lsssubg  14415  islss4  14420  issubrgd  14490  lidlsubg  14524  2idlcpblrng  14561  mplsubgfi  14744  lmtopcnp  15003  xmeter  15189  tgqioo  15308  suplociccreex  15377  dedekindicc  15386  ivthinclemlopn  15389  ivthinclemuopn  15391  sin0pilem2  15535  pilem3  15536  coseq0q4123  15587  uhgrissubgr  16141  egrsubgr  16143  uhgrspansubgr  16157  wlkres  16259