Theorem mpbir3an 1206

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

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

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 1007

This theorem is referenced by:  limon  4635  limom  4736  issmo  6519  xpider  6840  aptap  8924  5eluz3  9893  1eluzge0  9906  2eluzge1  9908  0elunit  10319  1elunit  10320  fz0to3un2pr  10457  4fvwrd4  10474  fzo0to42pr  10565  xnn0nnen  10799  resqrexlemga  11708  fprodge0  12323  fprodge1  12325  sincos1sgn  12451  sincos2sgn  12452  igz  13072  ballotfilem2  13142  qnnen  13182  strleun  13317  cnsubmlem  14726  cnsubglem  14727  cnsubrglem  14728  sinhalfpilem  15656  sincos4thpi  15705  sincos6thpi  15707  pigt3  15709  2logb9irr  15836  2logb9irrap  15842  konigsbergiedgwen  16479  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  konigsberglem4  16486