Theorem mpbir3an 1206

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

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

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 1007

This theorem is referenced by:  limon  4640  limom  4741  issmo  6532  xpider  6853  aptap  8941  5eluz3  9911  1eluzge0  9924  2eluzge1  9926  0elunit  10338  1elunit  10339  fz0to3un2pr  10479  4fvwrd4  10496  fzo0to42pr  10587  xnn0nnen  10823  resqrexlemga  11733  fprodge0  12348  fprodge1  12350  sincos1sgn  12476  sincos2sgn  12477  igz  13097  ballotfilem2  13172  ballotfilemth  13225  qnnen  13266  strleun  13401  cnsubmlem  14852  cnsubglem  14853  cnsubrglem  14854  sinhalfpilem  15782  sincos4thpi  15831  sincos6thpi  15833  pigt3  15835  2logb9irr  15962  2logb9irrap  15968  konigsbergiedgwen  16605  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  konigsberglem4  16612