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  4545  limom  4646  issmo  6341  xpider  6660  aptap  8669  1eluzge0  9639  2eluzge1  9641  0elunit  10052  1elunit  10053  fz0to3un2pr  10189  4fvwrd4  10206  fzo0to42pr  10287  xnn0nnen  10508  resqrexlemga  11167  fprodge0  11780  fprodge1  11782  sincos1sgn  11908  sincos2sgn  11909  igz  12512  qnnen  12588  strleun  12722  cnfldstr  14049  cnsubmlem  14066  cnsubglem  14067  cnsubrglem  14068  sinhalfpilem  14926  sincos4thpi  14975  sincos6thpi  14977  pigt3  14979  2logb9irr  15103  2logb9irrap  15109