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  10308  ixxss2  10309  ixxss12  10310  ubioc1  10333  lbico1  10334  lbicc2  10388  ubicc2  10389  lincmble  10408  elicod  10701  modqelico  10773  zmodfz  10785  modqmuladdim  10806  addmodid  10811  phicl2  12994  4sqlem12  13183  isstruct2r  13365  issubmd  13783  mndissubm  13784  submid  13786  subsubm  13792  0subm  13793  mhmima  13800  mhmeql  13801  issubgrpd2  13995  grpissubg  13999  subgintm  14003  nmzsubg  14015  eqger  14029  eqgcpbl  14033  ghmrn  14062  ghmpreima  14071  unitsubm  14428  subrgsubm  14544  subrgugrp  14550  subrgintm  14553  islssmd  14698  lsssubg  14716  islss4  14721  issubrgd  14791  lidlsubg  14825  2idlcpblrng  14862  mplsubgfi  15094  lmtopcnp  15353  xmeter  15539  tgqioo  15658  suplociccreex  15727  dedekindicc  15736  ivthinclemlopn  15739  ivthinclemuopn  15741  sin0pilem2  15886  pilem3  15887  coseq0q4123  15938  log2tlbndlog2  16088  uhgrissubgr  16514  egrsubgr  16516  uhgrspansubgr  16530  wlkres  16632