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  8696  1eluzge0  9667  2eluzge1  9669  0elunit  10080  1elunit  10081  fz0to3un2pr  10217  4fvwrd4  10234  fzo0to42pr  10315  xnn0nnen  10548  resqrexlemga  11207  fprodge0  11821  fprodge1  11823  sincos1sgn  11949  sincos2sgn  11950  igz  12570  qnnen  12675  strleun  12809  cnsubmlem  14212  cnsubglem  14213  cnsubrglem  14214  sinhalfpilem  15135  sincos4thpi  15184  sincos6thpi  15186  pigt3  15188  2logb9irr  15315  2logb9irrap  15321