Theorem mpbir3an 1205

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

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

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 1006

This theorem is referenced by:  limon  4611  limom  4712  issmo  6453  xpider  6774  aptap  8829  5eluz3  9794  1eluzge0  9807  2eluzge1  9809  0elunit  10220  1elunit  10221  fz0to3un2pr  10357  4fvwrd4  10374  fzo0to42pr  10464  xnn0nnen  10698  resqrexlemga  11583  fprodge0  12197  fprodge1  12199  sincos1sgn  12325  sincos2sgn  12326  igz  12946  qnnen  13051  strleun  13186  cnsubmlem  14591  cnsubglem  14592  cnsubrglem  14593  sinhalfpilem  15514  sincos4thpi  15563  sincos6thpi  15565  pigt3  15567  2logb9irr  15694  2logb9irrap  15700