Theorem mpbir3and 1206

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 1203	. 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 1004

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 1006

This theorem is referenced by:  ixxss1  10139  ixxss2  10140  ixxss12  10141  ubioc1  10164  lbico1  10165  lbicc2  10219  ubicc2  10220  elicod  10525  modqelico  10597  zmodfz  10609  modqmuladdim  10630  addmodid  10635  phicl2  12791  4sqlem12  12980  isstruct2r  13098  issubmd  13562  mndissubm  13563  submid  13565  subsubm  13571  0subm  13572  mhmima  13579  mhmeql  13580  issubgrpd2  13782  grpissubg  13786  subgintm  13790  nmzsubg  13802  eqger  13816  eqgcpbl  13820  ghmrn  13849  ghmpreima  13858  unitsubm  14139  subrgsubm  14254  subrgugrp  14260  subrgintm  14263  islssmd  14379  lsssubg  14397  islss4  14402  issubrgd  14472  lidlsubg  14506  2idlcpblrng  14543  mplsubgfi  14721  lmtopcnp  14980  xmeter  15166  tgqioo  15285  suplociccreex  15354  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemuopn  15368  sin0pilem2  15512  pilem3  15513  coseq0q4123  15564  uhgrissubgr  16118  egrsubgr  16120  uhgrspansubgr  16134  wlkres  16236