Theorem mpbir3an 1181

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

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

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 982

This theorem is referenced by:  limon  4550  limom  4651  issmo  6355  xpider  6674  aptap  8694  1eluzge0  9665  2eluzge1  9667  0elunit  10078  1elunit  10079  fz0to3un2pr  10215  4fvwrd4  10232  fzo0to42pr  10313  xnn0nnen  10546  resqrexlemga  11205  fprodge0  11819  fprodge1  11821  sincos1sgn  11947  sincos2sgn  11948  igz  12568  qnnen  12673  strleun  12807  cnsubmlem  14210  cnsubglem  14211  cnsubrglem  14212  sinhalfpilem  15111  sincos4thpi  15160  sincos6thpi  15162  pigt3  15164  2logb9irr  15291  2logb9irrap  15297