Theorem mpbir3an 1205

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

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

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 1006

This theorem is referenced by:  limon  4611  limom  4712  issmo  6454  xpider  6775  aptap  8830  5eluz3  9795  1eluzge0  9808  2eluzge1  9810  0elunit  10221  1elunit  10222  fz0to3un2pr  10358  4fvwrd4  10375  fzo0to42pr  10466  xnn0nnen  10700  resqrexlemga  11601  fprodge0  12216  fprodge1  12218  sincos1sgn  12344  sincos2sgn  12345  igz  12965  qnnen  13070  strleun  13205  cnsubmlem  14611  cnsubglem  14612  cnsubrglem  14613  sinhalfpilem  15534  sincos4thpi  15583  sincos6thpi  15585  pigt3  15587  2logb9irr  15714  2logb9irrap  15720  konigsbergiedgwen  16354  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberglem4  16361