Theorem mpbir3and 1183

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 1180	. 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 981

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 983

This theorem is referenced by:  ixxss1  10041  ixxss2  10042  ixxss12  10043  ubioc1  10066  lbico1  10067  lbicc2  10121  ubicc2  10122  elicod  10424  modqelico  10496  zmodfz  10508  modqmuladdim  10529  addmodid  10534  phicl2  12606  4sqlem12  12795  isstruct2r  12913  issubmd  13376  mndissubm  13377  submid  13379  subsubm  13385  0subm  13386  mhmima  13393  mhmeql  13394  issubgrpd2  13596  grpissubg  13600  subgintm  13604  nmzsubg  13616  eqger  13630  eqgcpbl  13634  ghmrn  13663  ghmpreima  13672  unitsubm  13951  subrgsubm  14066  subrgugrp  14072  subrgintm  14075  islssmd  14191  lsssubg  14209  islss4  14214  issubrgd  14284  lidlsubg  14318  2idlcpblrng  14355  mplsubgfi  14533  lmtopcnp  14792  xmeter  14978  tgqioo  15097  suplociccreex  15166  dedekindicc  15175  ivthinclemlopn  15178  ivthinclemuopn  15180  sin0pilem2  15324  pilem3  15325  coseq0q4123  15376