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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ixxss1  10317  ixxss2  10318  ixxss12  10319  ubioc1  10342  lbico1  10343  lbicc2  10397  ubicc2  10398  lincmble  10417  elicod  10710  modqelico  10786  zmodfz  10798  modqmuladdim  10819  addmodid  10824  phicl2  13015  4sqlem12  13204  isstruct2r  13415  issubmd  13834  mndissubm  13835  submid  13837  subsubm  13843  0subm  13844  mhmima  13851  mhmeql  13852  issubgrpd2  14046  grpissubg  14050  subgintm  14054  nmzsubg  14066  eqger  14080  eqgcpbl  14084  ghmrn  14113  ghmpreima  14122  cntzsubm  14164  unitsubm  14510  subrgsubm  14626  subrgugrp  14632  subrgintm  14635  islssmd  14780  lsssubg  14798  islss4  14803  issubrgd  14873  lidlsubg  14907  2idlcpblrng  14944  mplsubgfi  15183  lmtopcnp  15442  xmeter  15628  tgqioo  15747  suplociccreex  15816  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemuopn  15830  sin0pilem2  15975  pilem3  15976  coseq0q4123  16027  log2tlbndlog2  16186  uhgrissubgr  16673  egrsubgr  16675  uhgrspansubgr  16689  wlkres  16791