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  10322  ixxss2  10323  ixxss12  10324  ubioc1  10347  lbico1  10348  lbicc2  10402  ubicc2  10403  lincmble  10422  elicod  10715  modqelico  10791  zmodfz  10803  modqmuladdim  10824  addmodid  10829  phicl2  13020  4sqlem12  13209  isstruct2r  13420  issubmd  13839  mndissubm  13840  submid  13842  subsubm  13848  0subm  13849  mhmima  13856  mhmeql  13857  issubgrpd2  14051  grpissubg  14055  subgintm  14059  nmzsubg  14071  eqger  14085  eqgcpbl  14089  ghmrn  14118  ghmpreima  14127  cntzsubm  14169  unitsubm  14534  subrgsubm  14650  subrgugrp  14656  subrgintm  14659  islssmd  14804  lsssubg  14822  islss4  14827  issubrgd  14897  lidlsubg  14931  2idlcpblrng  14968  mplsubgfi  15234  lmtopcnp  15493  xmeter  15679  tgqioo  15798  suplociccreex  15867  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemuopn  15881  sin0pilem2  16026  pilem3  16027  coseq0q4123  16078  log2tlbndlog2  16237  uhgrissubgr  16724  egrsubgr  16726  uhgrspansubgr  16740  wlkres  16842