Theorem mpbir3and 1206

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

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

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 1006

This theorem is referenced by:  ixxss1  10139  ixxss2  10140  ixxss12  10141  ubioc1  10164  lbico1  10165  lbicc2  10219  ubicc2  10220  elicod  10525  modqelico  10597  zmodfz  10609  modqmuladdim  10630  addmodid  10635  phicl2  12788  4sqlem12  12977  isstruct2r  13095  issubmd  13559  mndissubm  13560  submid  13562  subsubm  13568  0subm  13569  mhmima  13576  mhmeql  13577  issubgrpd2  13779  grpissubg  13783  subgintm  13787  nmzsubg  13799  eqger  13813  eqgcpbl  13817  ghmrn  13846  ghmpreima  13855  unitsubm  14136  subrgsubm  14251  subrgugrp  14257  subrgintm  14260  islssmd  14376  lsssubg  14394  islss4  14399  issubrgd  14469  lidlsubg  14503  2idlcpblrng  14540  mplsubgfi  14718  lmtopcnp  14977  xmeter  15163  tgqioo  15282  suplociccreex  15351  dedekindicc  15360  ivthinclemlopn  15363  ivthinclemuopn  15365  sin0pilem2  15509  pilem3  15510  coseq0q4123  15561  uhgrissubgr  16115  egrsubgr  16117  uhgrspansubgr  16131  wlkres  16233