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	⊢ 𝜓
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 1202	. 2 ⊢ (𝜓 ∧ 𝜒 ∧ 𝜃)
5		mpbir3an.4	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	mpbir 146	1 ⊢ 𝜑

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  4640  limom  4741  issmo  6532  xpider  6853  aptap  8942  5eluz3  9914  1eluzge0  9927  2eluzge1  9929  0elunit  10341  1elunit  10342  fz0to3un2pr  10482  4fvwrd4  10499  fzo0to42pr  10590  xnn0nnen  10826  resqrexlemga  11736  fprodge0  12351  fprodge1  12353  sincos1sgn  12479  sincos2sgn  12480  igz  13100  ballotfilem2  13175  ballotfilemth  13228  qnnen  13269  strleun  13404  cnsubmlem  14855  cnsubglem  14856  cnsubrglem  14857  sinhalfpilem  15785  sincos4thpi  15834  sincos6thpi  15836  pigt3  15838  2logb9irr  15965  2logb9irrap  15971  konigsbergiedgwen  16608  konigsberglem1  16612  konigsberglem2  16613  konigsberglem3  16614  konigsberglem4  16615