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  10306  ixxss2  10307  ixxss12  10308  ubioc1  10331  lbico1  10332  lbicc2  10386  ubicc2  10387  lincmble  10406  elicod  10699  modqelico  10771  zmodfz  10783  modqmuladdim  10804  addmodid  10809  phicl2  12992  4sqlem12  13181  isstruct2r  13363  issubmd  13781  mndissubm  13782  submid  13784  subsubm  13790  0subm  13791  mhmima  13798  mhmeql  13799  issubgrpd2  13993  grpissubg  13997  subgintm  14001  nmzsubg  14013  eqger  14027  eqgcpbl  14031  ghmrn  14060  ghmpreima  14069  unitsubm  14426  subrgsubm  14542  subrgugrp  14548  subrgintm  14551  islssmd  14696  lsssubg  14714  islss4  14719  issubrgd  14789  lidlsubg  14823  2idlcpblrng  14860  mplsubgfi  15092  lmtopcnp  15351  xmeter  15537  tgqioo  15656  suplociccreex  15725  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemuopn  15739  sin0pilem2  15883  pilem3  15884  coseq0q4123  15935  log2tlbndlog2  16082  uhgrissubgr  16502  egrsubgr  16504  uhgrspansubgr  16518  wlkres  16620