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	⊢ 𝜓
mpbir3an.2	⊢ 𝜒
mpbir3an.3	⊢ 𝜃
mpbir3an.4	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
mpbir3an	⊢ 𝜑

Proof of Theorem mpbir3an

Step	Hyp	Ref	Expression
1		mpbir3an.1	. . 3 ⊢ 𝜓
2		mpbir3an.2	. . 3 ⊢ 𝜒
3		mpbir3an.3	. . 3 ⊢ 𝜃
4	1, 2, 3	3pm3.2i 1206	. 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃)
5		mpbir3an.4	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	mpbir 146	1 ⊢ 𝜑

Syntax hints:   ↔ wb 105   ∧ w3a 1009

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 1011

This theorem is referenced by:  limon  4658  limom  4759  issmo  6553  xpider  6874  aptap  8972  5eluz3  9944  1eluzge0  9957  2eluzge1  9959  0elunit  10371  1elunit  10372  fz0to3un2pr  10513  4fvwrd4  10530  fzo0to42pr  10621  xnn0nnen  10857  resqrexlemga  11772  fprodge0  12387  fprodge1  12389  sincos1sgn  12515  sincos2sgn  12516  igz  13136  ballotfilem2  13211  ballotfilemth  13264  qnnen  13305  strleun  13441  cnsubmlem  14898  cnsubglem  14899  cnsubrglem  14900  sinhalfpilem  15875  sincos4thpi  15924  sincos6thpi  15926  pigt3  15928  2logb9irr  16056  2logb9irrap  16062  konigsbergiedgwen  16708  konigsberglem1  16712  konigsberglem2  16713  konigsberglem3  16714  konigsberglem4  16715