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  4660  limom  4761  issmo  6559  xpider  6880  aptap  8981  5eluz3  9971  1eluzge0  9984  2eluzge1  9986  0elunit  10399  1elunit  10400  fz0to3un2pr  10541  4fvwrd4  10558  fzo0to42pr  10649  xnn0nnen  10889  resqrexlemga  11805  fprodge0  12423  fprodge1  12425  sincos1sgn  12551  sincos2sgn  12552  igz  13176  ballotfilem2  13280  ballotfilemth  13333  qnnen  13374  strleun  13511  cnsubmlem  14999  cnsubglem  15000  cnsubrglem  15001  sinhalfpilem  15984  sincos4thpi  16033  sincos6thpi  16035  pigt3  16037  2logb9irr  16168  2logb9irrap  16174  ppiublem1  16252  konigsbergiedgwen  16891  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem4  16898