Theorem mpbir3an 1203

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

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

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 1004

This theorem is referenced by:  limon  4604  limom  4705  issmo  6432  xpider  6751  aptap  8793  1eluzge0  9765  2eluzge1  9767  0elunit  10178  1elunit  10179  fz0to3un2pr  10315  4fvwrd4  10332  fzo0to42pr  10421  xnn0nnen  10654  resqrexlemga  11529  fprodge0  12143  fprodge1  12145  sincos1sgn  12271  sincos2sgn  12272  igz  12892  qnnen  12997  strleun  13132  cnsubmlem  14536  cnsubglem  14537  cnsubrglem  14538  sinhalfpilem  15459  sincos4thpi  15508  sincos6thpi  15510  pigt3  15512  2logb9irr  15639  2logb9irrap  15645