Theorem mpbir3and 1180

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 1177	. 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 978

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 980

This theorem is referenced by:  ixxss1  9907  ixxss2  9908  ixxss12  9909  ubioc1  9932  lbico1  9933  lbicc2  9987  ubicc2  9988  elicod  10268  modqelico  10337  zmodfz  10349  modqmuladdim  10370  addmodid  10375  phicl2  12217  isstruct2r  12476  issubmd  12873  mndissubm  12874  submid  12876  0subm  12879  mhmima  12883  mhmeql  12884  issubgrpd2  13064  grpissubg  13068  subgintm  13072  nmzsubg  13084  eqger  13098  eqgcpbl  13102  unitsubm  13326  subrgsubm  13393  subrgugrp  13399  subrgintm  13402  islssmd  13484  lsssubg  13502  islss4  13507  issubrgd  13577  lidlsubg  13605  lmtopcnp  13938  xmeter  14124  tgqioo  14235  suplociccreex  14290  dedekindicc  14299  ivthinclemlopn  14302  ivthinclemuopn  14304  sin0pilem2  14391  pilem3  14392  coseq0q4123  14443