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  4549  limom  4650  issmo  6346  xpider  6665  aptap  8677  1eluzge0  9648  2eluzge1  9650  0elunit  10061  1elunit  10062  fz0to3un2pr  10198  4fvwrd4  10215  fzo0to42pr  10296  xnn0nnen  10529  resqrexlemga  11188  fprodge0  11802  fprodge1  11804  sincos1sgn  11930  sincos2sgn  11931  igz  12543  qnnen  12648  strleun  12782  cnsubmlem  14134  cnsubglem  14135  cnsubrglem  14136  sinhalfpilem  15027  sincos4thpi  15076  sincos6thpi  15078  pigt3  15080  2logb9irr  15207  2logb9irrap  15213