Theorem mpbir3an 1179

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

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

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 980

This theorem is referenced by:  limon  4514  limom  4615  issmo  6291  xpider  6608  aptap  8609  1eluzge0  9576  2eluzge1  9578  0elunit  9988  1elunit  9989  fz0to3un2pr  10125  4fvwrd4  10142  fzo0to42pr  10222  resqrexlemga  11034  fprodge0  11647  fprodge1  11649  sincos1sgn  11774  sincos2sgn  11775  igz  12374  qnnen  12434  strleun  12565  cnfldstr  13496  cnsubmlem  13511  cnsubglem  13512  cnsubrglem  13513  sinhalfpilem  14251  sincos4thpi  14300  sincos6thpi  14302  pigt3  14304  2logb9irr  14428  2logb9irrap  14434