Theorem mpbir3and 1175

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 1172	. 2 |- ( ph -> ( ch /\ th /\ ta ) )
5		mpbir3and.4	. 2 |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )
6	4, 5	mpbird 166	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 104   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  ixxss1  9861  ixxss2  9862  ixxss12  9863  ubioc1  9886  lbico1  9887  lbicc2  9941  ubicc2  9942  elicod  10221  modqelico  10290  zmodfz  10302  modqmuladdim  10323  addmodid  10328  phicl2  12168  isstruct2r  12427  issubmd  12696  mndissubm  12697  submid  12699  0subm  12702  mhmima  12706  mhmeql  12707  lmtopcnp  13044  xmeter  13230  tgqioo  13341  suplociccreex  13396  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemuopn  13410  sin0pilem2  13497  pilem3  13498  coseq0q4123  13549