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  4495  limom  4596  issmo  6265  xpider  6582  1eluzge0  9526  2eluzge1  9528  0elunit  9936  1elunit  9937  fz0to3un2pr  10072  4fvwrd4  10089  fzo0to42pr  10169  resqrexlemga  10980  fprodge0  11593  fprodge1  11595  sincos1sgn  11720  sincos2sgn  11721  igz  12319  qnnen  12379  strleun  12500  sinhalfpilem  13471  sincos4thpi  13520  sincos6thpi  13522  pigt3  13524  2logb9irr  13648  2logb9irrap  13654