Theorem mpbir3and 1204

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 1201	. 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 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  10088  ixxss2  10089  ixxss12  10090  ubioc1  10113  lbico1  10114  lbicc2  10168  ubicc2  10169  elicod  10471  modqelico  10543  zmodfz  10555  modqmuladdim  10576  addmodid  10581  phicl2  12722  4sqlem12  12911  isstruct2r  13029  issubmd  13493  mndissubm  13494  submid  13496  subsubm  13502  0subm  13503  mhmima  13510  mhmeql  13511  issubgrpd2  13713  grpissubg  13717  subgintm  13721  nmzsubg  13733  eqger  13747  eqgcpbl  13751  ghmrn  13780  ghmpreima  13789  unitsubm  14068  subrgsubm  14183  subrgugrp  14189  subrgintm  14192  islssmd  14308  lsssubg  14326  islss4  14331  issubrgd  14401  lidlsubg  14435  2idlcpblrng  14472  mplsubgfi  14650  lmtopcnp  14909  xmeter  15095  tgqioo  15214  suplociccreex  15283  dedekindicc  15292  ivthinclemlopn  15295  ivthinclemuopn  15297  sin0pilem2  15441  pilem3  15442  coseq0q4123  15493