Theorem mpbir3an 1168

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

Syntax hints:   <-> wb 104   /\ w3a 967

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 969

This theorem is referenced by:  limon  4484  limom  4585  issmo  6247  xpider  6563  1eluzge0  9503  2eluzge1  9505  0elunit  9913  1elunit  9914  fz0to3un2pr  10048  4fvwrd4  10065  fzo0to42pr  10145  resqrexlemga  10951  fprodge0  11564  fprodge1  11566  sincos1sgn  11691  sincos2sgn  11692  qnnen  12301  strleun  12420  sinhalfpilem  13253  sincos4thpi  13302  sincos6thpi  13304  pigt3  13306  2logb9irr  13430  2logb9irrap  13436