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 ⊢ 𝜑

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  8979  5eluz3  9963  1eluzge0  9976  2eluzge1  9978  0elunit  10390  1elunit  10391  fz0to3un2pr  10532  4fvwrd4  10549  fzo0to42pr  10640  xnn0nnen  10876  resqrexlemga  11791  fprodge0  12406  fprodge1  12408  sincos1sgn  12534  sincos2sgn  12535  igz  13155  ballotfilem2  13230  ballotfilemth  13283  qnnen  13324  strleun  13460  cnsubmlem  14917  cnsubglem  14918  cnsubrglem  14919  sinhalfpilem  15895  sincos4thpi  15944  sincos6thpi  15946  pigt3  15948  2logb9irr  16079  2logb9irrap  16085  konigsbergiedgwen  16737  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberglem4  16744