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  4605  limom  4706  issmo  6440  xpider  6761  aptap  8808  1eluzge0  9781  2eluzge1  9783  0elunit  10194  1elunit  10195  fz0to3un2pr  10331  4fvwrd4  10348  fzo0to42pr  10438  xnn0nnen  10671  resqrexlemga  11549  fprodge0  12163  fprodge1  12165  sincos1sgn  12291  sincos2sgn  12292  igz  12912  qnnen  13017  strleun  13152  cnsubmlem  14557  cnsubglem  14558  cnsubrglem  14559  sinhalfpilem  15480  sincos4thpi  15529  sincos6thpi  15531  pigt3  15533  2logb9irr  15660  2logb9irrap  15666