Theorem mpbir3an 1203

Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.)

Hypotheses

Ref	Expression
mpbir3an.1	|- ps
mpbir3an.2	|- ch
mpbir3an.3	|- th
mpbir3an.4	|- ( ph <-> ( ps /\ ch /\ th ) )

Assertion

Ref	Expression
mpbir3an	|- ph

Proof of Theorem mpbir3an

Step	Hyp	Ref	Expression
1		mpbir3an.1	. . 3 |- ps
2		mpbir3an.2	. . 3 |- ch
3		mpbir3an.3	. . 3 |- th
4	1, 2, 3	3pm3.2i 1199	. 2 |- ( ps /\ ch /\ th )
5		mpbir3an.4	. 2 |- ( ph <-> ( ps /\ ch /\ th ) )
6	4, 5	mpbir 146	1 |- ph

Syntax hints:   <-> wb 105   /\ w3a 1002

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 1004

This theorem is referenced by:  limon  4609  limom  4710  issmo  6449  xpider  6770  aptap  8820  5eluz3  9785  1eluzge0  9798  2eluzge1  9800  0elunit  10211  1elunit  10212  fz0to3un2pr  10348  4fvwrd4  10365  fzo0to42pr  10455  xnn0nnen  10689  resqrexlemga  11574  fprodge0  12188  fprodge1  12190  sincos1sgn  12316  sincos2sgn  12317  igz  12937  qnnen  13042  strleun  13177  cnsubmlem  14582  cnsubglem  14583  cnsubrglem  14584  sinhalfpilem  15505  sincos4thpi  15554  sincos6thpi  15556  pigt3  15558  2logb9irr  15685  2logb9irrap  15691