Theorem mpbir3and 1182

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

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

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 982

This theorem is referenced by:  ixxss1  9924  ixxss2  9925  ixxss12  9926  ubioc1  9949  lbico1  9950  lbicc2  10004  ubicc2  10005  elicod  10285  modqelico  10354  zmodfz  10366  modqmuladdim  10387  addmodid  10392  phicl2  12234  4sqlem12  12417  isstruct2r  12498  issubmd  12899  mndissubm  12900  submid  12902  subsubm  12908  0subm  12909  mhmima  12916  mhmeql  12917  issubgrpd2  13102  grpissubg  13106  subgintm  13110  nmzsubg  13122  eqger  13136  eqgcpbl  13140  ghmrn  13164  ghmpreima  13173  unitsubm  13437  subrgsubm  13549  subrgugrp  13555  subrgintm  13558  islssmd  13643  lsssubg  13661  islss4  13666  issubrgd  13736  lidlsubg  13770  2idlcpblrng  13806  lmtopcnp  14154  xmeter  14340  tgqioo  14451  suplociccreex  14506  dedekindicc  14515  ivthinclemlopn  14518  ivthinclemuopn  14520  sin0pilem2  14607  pilem3  14608  coseq0q4123  14659