Theorem mpbir3and 1182

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

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

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 982

This theorem is referenced by:  ixxss1  9922  ixxss2  9923  ixxss12  9924  ubioc1  9947  lbico1  9948  lbicc2  10002  ubicc2  10003  elicod  10283  modqelico  10352  zmodfz  10364  modqmuladdim  10385  addmodid  10390  phicl2  12232  isstruct2r  12491  issubmd  12892  mndissubm  12893  submid  12895  subsubm  12901  0subm  12902  mhmima  12909  mhmeql  12910  issubgrpd2  13095  grpissubg  13099  subgintm  13103  nmzsubg  13115  eqger  13129  eqgcpbl  13133  ghmrn  13157  ghmpreima  13166  unitsubm  13430  subrgsubm  13542  subrgugrp  13548  subrgintm  13551  islssmd  13636  lsssubg  13654  islss4  13659  issubrgd  13729  lidlsubg  13763  2idlcpblrng  13799  lmtopcnp  14147  xmeter  14333  tgqioo  14444  suplociccreex  14499  dedekindicc  14508  ivthinclemlopn  14511  ivthinclemuopn  14513  sin0pilem2  14600  pilem3  14601  coseq0q4123  14652