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  8978  5eluz3  9961  1eluzge0  9974  2eluzge1  9976  0elunit  10388  1elunit  10389  fz0to3un2pr  10530  4fvwrd4  10547  fzo0to42pr  10638  xnn0nnen  10874  resqrexlemga  11789  fprodge0  12404  fprodge1  12406  sincos1sgn  12532  sincos2sgn  12533  igz  13153  ballotfilem2  13228  ballotfilemth  13281  qnnen  13322  strleun  13458  cnsubmlem  14915  cnsubglem  14916  cnsubrglem  14917  sinhalfpilem  15892  sincos4thpi  15941  sincos6thpi  15943  pigt3  15945  2logb9irr  16073  2logb9irrap  16079  konigsbergiedgwen  16725  konigsberglem1  16729  konigsberglem2  16730  konigsberglem3  16731  konigsberglem4  16732