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  10117  ixxss2  10118  ixxss12  10119  ubioc1  10142  lbico1  10143  lbicc2  10197  ubicc2  10198  elicod  10501  modqelico  10573  zmodfz  10585  modqmuladdim  10606  addmodid  10611  phicl2  12757  4sqlem12  12946  isstruct2r  13064  issubmd  13528  mndissubm  13529  submid  13531  subsubm  13537  0subm  13538  mhmima  13545  mhmeql  13546  issubgrpd2  13748  grpissubg  13752  subgintm  13756  nmzsubg  13768  eqger  13782  eqgcpbl  13786  ghmrn  13815  ghmpreima  13824  unitsubm  14104  subrgsubm  14219  subrgugrp  14225  subrgintm  14228  islssmd  14344  lsssubg  14362  islss4  14367  issubrgd  14437  lidlsubg  14471  2idlcpblrng  14508  mplsubgfi  14686  lmtopcnp  14945  xmeter  15131  tgqioo  15250  suplociccreex  15319  dedekindicc  15328  ivthinclemlopn  15331  ivthinclemuopn  15333  sin0pilem2  15477  pilem3  15478  coseq0q4123  15529  wlkres  16149