Theorem mpbir3and 1211

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ixxss1  10316  ixxss2  10317  ixxss12  10318  ubioc1  10341  lbico1  10342  lbicc2  10396  ubicc2  10397  lincmble  10416  elicod  10709  modqelico  10784  zmodfz  10796  modqmuladdim  10817  addmodid  10822  phicl2  13012  4sqlem12  13201  isstruct2r  13412  issubmd  13830  mndissubm  13831  submid  13833  subsubm  13839  0subm  13840  mhmima  13847  mhmeql  13848  issubgrpd2  14042  grpissubg  14046  subgintm  14050  nmzsubg  14062  eqger  14076  eqgcpbl  14080  ghmrn  14109  ghmpreima  14118  unitsubm  14475  subrgsubm  14591  subrgugrp  14597  subrgintm  14600  islssmd  14745  lsssubg  14763  islss4  14768  issubrgd  14838  lidlsubg  14872  2idlcpblrng  14909  mplsubgfi  15141  lmtopcnp  15400  xmeter  15586  tgqioo  15705  suplociccreex  15774  dedekindicc  15783  ivthinclemlopn  15786  ivthinclemuopn  15788  sin0pilem2  15933  pilem3  15934  coseq0q4123  15985  log2tlbndlog2  16139  uhgrissubgr  16621  egrsubgr  16623  uhgrspansubgr  16637  wlkres  16739