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  4634  limom  4735  issmo  6518  xpider  6839  aptap  8920  5eluz3  9889  1eluzge0  9902  2eluzge1  9904  0elunit  10315  1elunit  10316  fz0to3un2pr  10453  4fvwrd4  10470  fzo0to42pr  10561  xnn0nnen  10795  resqrexlemga  11701  fprodge0  12316  fprodge1  12318  sincos1sgn  12444  sincos2sgn  12445  igz  13065  qnnen  13171  strleun  13306  cnsubmlem  14713  cnsubglem  14714  cnsubrglem  14715  sinhalfpilem  15643  sincos4thpi  15692  sincos6thpi  15694  pigt3  15696  2logb9irr  15823  2logb9irrap  15829  konigsbergiedgwen  16466  konigsberglem1  16470  konigsberglem2  16471  konigsberglem3  16472  konigsberglem4  16473