Theorem mpbir3and 1182

Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
mpbir3and.1	|- ( ph -> ch )
mpbir3and.2	|- ( ph -> th )
mpbir3and.3	|- ( ph -> ta )
mpbir3and.4	|- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )

Assertion

Ref	Expression
mpbir3and	|- ( ph -> ps )

Proof of Theorem mpbir3and

Step	Hyp	Ref	Expression
1		mpbir3and.1	. . 3 |- ( ph -> ch )
2		mpbir3and.2	. . 3 |- ( ph -> th )
3		mpbir3and.3	. . 3 |- ( ph -> ta )
4	1, 2, 3	3jca 1179	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
5		mpbir3and.4	. 2 |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
6	4, 5	mpbird 167	1 |- ( ph -> ps )

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  9970  ixxss2  9971  ixxss12  9972  ubioc1  9995  lbico1  9996  lbicc2  10050  ubicc2  10051  elicod  10333  modqelico  10405  zmodfz  10417  modqmuladdim  10438  addmodid  10443  phicl2  12352  4sqlem12  12540  isstruct2r  12629  issubmd  13046  mndissubm  13047  submid  13049  subsubm  13055  0subm  13056  mhmima  13063  mhmeql  13064  issubgrpd2  13260  grpissubg  13264  subgintm  13268  nmzsubg  13280  eqger  13294  eqgcpbl  13298  ghmrn  13327  ghmpreima  13336  unitsubm  13615  subrgsubm  13730  subrgugrp  13736  subrgintm  13739  islssmd  13855  lsssubg  13873  islss4  13878  issubrgd  13948  lidlsubg  13982  2idlcpblrng  14019  lmtopcnp  14418  xmeter  14604  tgqioo  14715  suplociccreex  14778  dedekindicc  14787  ivthinclemlopn  14790  ivthinclemuopn  14792  sin0pilem2  14917  pilem3  14918  coseq0q4123  14969