Theorem mpbir3and 1181

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

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

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 981

This theorem is referenced by:  ixxss1  9918  ixxss2  9919  ixxss12  9920  ubioc1  9943  lbico1  9944  lbicc2  9998  ubicc2  9999  elicod  10279  modqelico  10348  zmodfz  10360  modqmuladdim  10381  addmodid  10386  phicl2  12228  isstruct2r  12487  issubmd  12887  mndissubm  12888  submid  12890  0subm  12893  mhmima  12897  mhmeql  12898  issubgrpd2  13082  grpissubg  13086  subgintm  13090  nmzsubg  13102  eqger  13116  eqgcpbl  13120  unitsubm  13367  subrgsubm  13454  subrgugrp  13460  subrgintm  13463  islssmd  13548  lsssubg  13566  islss4  13571  issubrgd  13641  lidlsubg  13675  2idlcpblrng  13711  lmtopcnp  14046  xmeter  14232  tgqioo  14343  suplociccreex  14398  dedekindicc  14407  ivthinclemlopn  14410  ivthinclemuopn  14412  sin0pilem2  14499  pilem3  14500  coseq0q4123  14551