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

This proof depends on syntax axioms:   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  limon  4662  limom  4763  issmo  6564  xpider  6885  aptap  8986  5eluz3  9976  1eluzge0  9989  2eluzge1  9991  0elunit  10404  1elunit  10405  fz0to3un2pr  10546  4fvwrd4  10563  fzo0to42pr  10654  xnn0nnen  10894  resqrexlemga  11810  fprodge0  12428  fprodge1  12430  sincos1sgn  12556  sincos2sgn  12557  igz  13181  ballotfilem2  13285  ballotfilemth  13338  qnnen  13379  strleun  13516  cnsubmlem  15023  cnsubglem  15024  cnsubrglem  15025  sinhalfpilem  16035  sincos4thpi  16084  sincos6thpi  16086  pigt3  16088  2logb9irr  16224  2logb9irrap  16230  ppiublem1  16308  konigsbergiedgwen  16947  konigsberglem1  16951  konigsberglem2  16952  konigsberglem3  16953  konigsberglem4  16954