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  9979  ixxss2  9980  ixxss12  9981  ubioc1  10004  lbico1  10005  lbicc2  10059  ubicc2  10060  elicod  10354  modqelico  10426  zmodfz  10438  modqmuladdim  10459  addmodid  10464  phicl2  12382  4sqlem12  12571  isstruct2r  12689  issubmd  13106  mndissubm  13107  submid  13109  subsubm  13115  0subm  13116  mhmima  13123  mhmeql  13124  issubgrpd2  13320  grpissubg  13324  subgintm  13328  nmzsubg  13340  eqger  13354  eqgcpbl  13358  ghmrn  13387  ghmpreima  13396  unitsubm  13675  subrgsubm  13790  subrgugrp  13796  subrgintm  13799  islssmd  13915  lsssubg  13933  islss4  13938  issubrgd  14008  lidlsubg  14042  2idlcpblrng  14079  lmtopcnp  14486  xmeter  14672  tgqioo  14791  suplociccreex  14860  dedekindicc  14869  ivthinclemlopn  14872  ivthinclemuopn  14874  sin0pilem2  15018  pilem3  15019  coseq0q4123  15070