Theorem mpbir3an 1210

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

This proof depends on syntax axioms:   <-> wb 105   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  limon  4660  limom  4761  issmo  6559  xpider  6880  aptap  8980  5eluz3  9970  1eluzge0  9983  2eluzge1  9985  0elunit  10398  1elunit  10399  fz0to3un2pr  10540  4fvwrd4  10557  fzo0to42pr  10648  xnn0nnen  10887  resqrexlemga  11803  fprodge0  12420  fprodge1  12422  sincos1sgn  12548  sincos2sgn  12549  igz  13173  ballotfilem2  13277  ballotfilemth  13330  qnnen  13371  strleun  13507  cnsubmlem  14964  cnsubglem  14965  cnsubrglem  14966  sinhalfpilem  15942  sincos4thpi  15991  sincos6thpi  15993  pigt3  15995  2logb9irr  16126  2logb9irrap  16132  ppiublem1  16192  konigsbergiedgwen  16823  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberglem4  16830