Theorem mpbir3an 1182

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

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

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 983

This theorem is referenced by:  limon  4569  limom  4670  issmo  6387  xpider  6706  aptap  8743  1eluzge0  9715  2eluzge1  9717  0elunit  10128  1elunit  10129  fz0to3un2pr  10265  4fvwrd4  10282  fzo0to42pr  10371  xnn0nnen  10604  resqrexlemga  11409  fprodge0  12023  fprodge1  12025  sincos1sgn  12151  sincos2sgn  12152  igz  12772  qnnen  12877  strleun  13011  cnsubmlem  14415  cnsubglem  14416  cnsubrglem  14417  sinhalfpilem  15338  sincos4thpi  15387  sincos6thpi  15389  pigt3  15391  2logb9irr  15518  2logb9irrap  15524