Theorem mpbir3and 1207

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

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

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 1007

This theorem is referenced by:  ixxss1  10233  ixxss2  10234  ixxss12  10235  ubioc1  10258  lbico1  10259  lbicc2  10313  ubicc2  10314  lincmble  10333  elicod  10620  modqelico  10692  zmodfz  10704  modqmuladdim  10725  addmodid  10730  phicl2  12904  4sqlem12  13093  isstruct2r  13212  issubmd  13676  mndissubm  13677  submid  13679  subsubm  13685  0subm  13686  mhmima  13693  mhmeql  13694  issubgrpd2  13896  grpissubg  13900  subgintm  13904  nmzsubg  13916  eqger  13930  eqgcpbl  13934  ghmrn  13963  ghmpreima  13972  unitsubm  14253  subrgsubm  14368  subrgugrp  14374  subrgintm  14377  islssmd  14494  lsssubg  14512  islss4  14517  issubrgd  14587  lidlsubg  14621  2idlcpblrng  14658  mplsubgfi  14843  lmtopcnp  15102  xmeter  15288  tgqioo  15407  suplociccreex  15476  dedekindicc  15485  ivthinclemlopn  15488  ivthinclemuopn  15490  sin0pilem2  15634  pilem3  15635  coseq0q4123  15686  uhgrissubgr  16243  egrsubgr  16245  uhgrspansubgr  16259  wlkres  16361