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  4662  limom  4763  issmo  6563  xpider  6884  aptap  8986  5eluz3  9977  1eluzge0  9990  2eluzge1  9992  0elunit  10405  1elunit  10406  fz0to3un2pr  10547  4fvwrd4  10564  fzo0to42pr  10655  xnn0nnen  10895  resqrexlemga  11811  fprodge0  12429  fprodge1  12431  sincos1sgn  12557  sincos2sgn  12558  igz  13182  ballotfilem2  13286  ballotfilemth  13339  qnnen  13380  strleun  13517  cnsubmlem  15024  cnsubglem  15025  cnsubrglem  15026  sinhalfpilem  16018  sincos4thpi  16067  sincos6thpi  16069  pigt3  16071  2logb9irr  16207  2logb9irrap  16213  ppiublem1  16291  konigsbergiedgwen  16930  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberglem4  16937