Theorem mpbir3an 1210

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

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

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 1011

This theorem is referenced by:  limon  4655  limom  4756  issmo  6549  xpider  6870  aptap  8968  5eluz3  9940  1eluzge0  9953  2eluzge1  9955  0elunit  10367  1elunit  10368  fz0to3un2pr  10508  4fvwrd4  10525  fzo0to42pr  10616  xnn0nnen  10852  resqrexlemga  11767  fprodge0  12382  fprodge1  12384  sincos1sgn  12510  sincos2sgn  12511  igz  13131  ballotfilem2  13206  ballotfilemth  13259  qnnen  13300  strleun  13435  cnsubmlem  14887  cnsubglem  14888  cnsubrglem  14889  sinhalfpilem  15815  sincos4thpi  15864  sincos6thpi  15866  pigt3  15868  2logb9irr  15996  2logb9irrap  16002  konigsbergiedgwen  16639  konigsberglem1  16643  konigsberglem2  16644  konigsberglem3  16645  konigsberglem4  16646