Theorem mpbir3an 1174

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 1170	. 2 |- ( ps /\ ch /\ th )
5		mpbir3an.4	. 2 |- ( ph <-> ( ps /\ ch /\ th ) )
6	4, 5	mpbir 145	1 |- ph

Syntax hints:   <-> 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:  limon  4497  limom  4598  issmo  6267  xpider  6584  1eluzge0  9533  2eluzge1  9535  0elunit  9943  1elunit  9944  fz0to3un2pr  10079  4fvwrd4  10096  fzo0to42pr  10176  resqrexlemga  10987  fprodge0  11600  fprodge1  11602  sincos1sgn  11727  sincos2sgn  11728  igz  12326  qnnen  12386  strleun  12507  sinhalfpilem  13506  sincos4thpi  13555  sincos6thpi  13557  pigt3  13559  2logb9irr  13683  2logb9irrap  13689