Theorem mpbir3an 1169

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

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

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 970

This theorem is referenced by:  limon  4490  limom  4591  issmo  6256  xpider  6572  1eluzge0  9512  2eluzge1  9514  0elunit  9922  1elunit  9923  fz0to3un2pr  10058  4fvwrd4  10075  fzo0to42pr  10155  resqrexlemga  10965  fprodge0  11578  fprodge1  11580  sincos1sgn  11705  sincos2sgn  11706  igz  12304  qnnen  12364  strleun  12484  sinhalfpilem  13352  sincos4thpi  13401  sincos6thpi  13403  pigt3  13405  2logb9irr  13529  2logb9irrap  13535