Theorem mpbir3an 1163

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

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

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 964

This theorem is referenced by:  limon  4429  limom  4527  issmo  6185  xpider  6500  1eluzge0  9372  2eluzge1  9374  0elunit  9772  1elunit  9773  4fvwrd4  9920  fzo0to42pr  10000  resqrexlemga  10798  sincos1sgn  11474  sincos2sgn  11475  qnnen  11947  strleun  12051  sinhalfpilem  12875  sincos4thpi  12924  sincos6thpi  12926  pigt3  12928