Theorem mpbir3and 1204

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

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

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 1004

This theorem is referenced by:  ixxss1  10132  ixxss2  10133  ixxss12  10134  ubioc1  10157  lbico1  10158  lbicc2  10212  ubicc2  10213  elicod  10517  modqelico  10589  zmodfz  10601  modqmuladdim  10622  addmodid  10627  phicl2  12779  4sqlem12  12968  isstruct2r  13086  issubmd  13550  mndissubm  13551  submid  13553  subsubm  13559  0subm  13560  mhmima  13567  mhmeql  13568  issubgrpd2  13770  grpissubg  13774  subgintm  13778  nmzsubg  13790  eqger  13804  eqgcpbl  13808  ghmrn  13837  ghmpreima  13846  unitsubm  14126  subrgsubm  14241  subrgugrp  14247  subrgintm  14250  islssmd  14366  lsssubg  14384  islss4  14389  issubrgd  14459  lidlsubg  14493  2idlcpblrng  14530  mplsubgfi  14708  lmtopcnp  14967  xmeter  15153  tgqioo  15272  suplociccreex  15341  dedekindicc  15350  ivthinclemlopn  15353  ivthinclemuopn  15355  sin0pilem2  15499  pilem3  15500  coseq0q4123  15551  wlkres  16188