Theorem mpbir3an 1181

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

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

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 982

This theorem is referenced by:  limon  4546  limom  4647  issmo  6343  xpider  6662  aptap  8671  1eluzge0  9642  2eluzge1  9644  0elunit  10055  1elunit  10056  fz0to3un2pr  10192  4fvwrd4  10209  fzo0to42pr  10290  xnn0nnen  10511  resqrexlemga  11170  fprodge0  11783  fprodge1  11785  sincos1sgn  11911  sincos2sgn  11912  igz  12515  qnnen  12591  strleun  12725  cnsubmlem  14077  cnsubglem  14078  cnsubrglem  14079  sinhalfpilem  14967  sincos4thpi  15016  sincos6thpi  15018  pigt3  15020  2logb9irr  15144  2logb9irrap  15150