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 ⊢ (𝜑 → 𝜓)

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

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 1011

This theorem is referenced by:  ixxss1  10289  ixxss2  10290  ixxss12  10291  ubioc1  10314  lbico1  10315  lbicc2  10369  ubicc2  10370  lincmble  10389  elicod  10682  modqelico  10754  zmodfz  10766  modqmuladdim  10787  addmodid  10792  phicl2  12975  4sqlem12  13164  isstruct2r  13346  issubmd  13764  mndissubm  13765  submid  13767  subsubm  13773  0subm  13774  mhmima  13781  mhmeql  13782  issubgrpd2  13976  grpissubg  13980  subgintm  13984  nmzsubg  13996  eqger  14010  eqgcpbl  14014  ghmrn  14043  ghmpreima  14052  unitsubm  14409  subrgsubm  14525  subrgugrp  14531  subrgintm  14534  islssmd  14679  lsssubg  14697  islss4  14702  issubrgd  14772  lidlsubg  14806  2idlcpblrng  14843  mplsubgfi  15075  lmtopcnp  15334  xmeter  15520  tgqioo  15639  suplociccreex  15708  dedekindicc  15717  ivthinclemlopn  15720  ivthinclemuopn  15722  sin0pilem2  15866  pilem3  15867  coseq0q4123  15918  log2tlbndlog2  16065  uhgrissubgr  16485  egrsubgr  16487  uhgrspansubgr  16501  wlkres  16603