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  4617  limom  4718  issmo  6497  xpider  6818  aptap  8872  5eluz3  9839  1eluzge0  9852  2eluzge1  9854  0elunit  10265  1elunit  10266  fz0to3un2pr  10403  4fvwrd4  10420  fzo0to42pr  10511  xnn0nnen  10745  resqrexlemga  11646  fprodge0  12261  fprodge1  12263  sincos1sgn  12389  sincos2sgn  12390  igz  13010  qnnen  13115  strleun  13250  cnsubmlem  14657  cnsubglem  14658  cnsubrglem  14659  sinhalfpilem  15585  sincos4thpi  15634  sincos6thpi  15636  pigt3  15638  2logb9irr  15765  2logb9irrap  15771  konigsbergiedgwen  16408  konigsberglem1  16412  konigsberglem2  16413  konigsberglem3  16414  konigsberglem4  16415