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  9996  ixxss2  9997  ixxss12  9998  ubioc1  10021  lbico1  10022  lbicc2  10076  ubicc2  10077  elicod  10371  modqelico  10443  zmodfz  10455  modqmuladdim  10476  addmodid  10481  phicl2  12407  4sqlem12  12596  isstruct2r  12714  issubmd  13176  mndissubm  13177  submid  13179  subsubm  13185  0subm  13186  mhmima  13193  mhmeql  13194  issubgrpd2  13396  grpissubg  13400  subgintm  13404  nmzsubg  13416  eqger  13430  eqgcpbl  13434  ghmrn  13463  ghmpreima  13472  unitsubm  13751  subrgsubm  13866  subrgugrp  13872  subrgintm  13875  islssmd  13991  lsssubg  14009  islss4  14014  issubrgd  14084  lidlsubg  14118  2idlcpblrng  14155  lmtopcnp  14570  xmeter  14756  tgqioo  14875  suplociccreex  14944  dedekindicc  14953  ivthinclemlopn  14956  ivthinclemuopn  14958  sin0pilem2  15102  pilem3  15103  coseq0q4123  15154