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  9998  ixxss2  9999  ixxss12  10000  ubioc1  10023  lbico1  10024  lbicc2  10078  ubicc2  10079  elicod  10373  modqelico  10445  zmodfz  10457  modqmuladdim  10478  addmodid  10483  phicl2  12409  4sqlem12  12598  isstruct2r  12716  issubmd  13178  mndissubm  13179  submid  13181  subsubm  13187  0subm  13188  mhmima  13195  mhmeql  13196  issubgrpd2  13398  grpissubg  13402  subgintm  13406  nmzsubg  13418  eqger  13432  eqgcpbl  13436  ghmrn  13465  ghmpreima  13474  unitsubm  13753  subrgsubm  13868  subrgugrp  13874  subrgintm  13877  islssmd  13993  lsssubg  14011  islss4  14016  issubrgd  14086  lidlsubg  14120  2idlcpblrng  14157  lmtopcnp  14572  xmeter  14758  tgqioo  14877  suplociccreex  14946  dedekindicc  14955  ivthinclemlopn  14958  ivthinclemuopn  14960  sin0pilem2  15104  pilem3  15105  coseq0q4123  15156