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  4559  limom  4660  issmo  6364  xpider  6683  aptap  8705  1eluzge0  9677  2eluzge1  9679  0elunit  10090  1elunit  10091  fz0to3un2pr  10227  4fvwrd4  10244  fzo0to42pr  10330  xnn0nnen  10563  resqrexlemga  11253  fprodge0  11867  fprodge1  11869  sincos1sgn  11995  sincos2sgn  11996  igz  12616  qnnen  12721  strleun  12855  cnsubmlem  14258  cnsubglem  14259  cnsubrglem  14260  sinhalfpilem  15181  sincos4thpi  15230  sincos6thpi  15232  pigt3  15234  2logb9irr  15361  2logb9irrap  15367