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  4662  limom  4763  issmo  6563  xpider  6884  aptap  8987  5eluz3  9978  1eluzge0  9991  2eluzge1  9993  0elunit  10406  1elunit  10407  fz0to3un2pr  10548  4fvwrd4  10565  fzo0to42pr  10656  xnn0nnen  10896  resqrexlemga  11812  fprodge0  12430  fprodge1  12432  sincos1sgn  12558  sincos2sgn  12559  igz  13183  ballotfilem2  13287  ballotfilemth  13340  qnnen  13381  strleun  13518  cnsubmlem  15025  cnsubglem  15026  cnsubrglem  15027  sinhalfpilem  16030  sincos4thpi  16079  sincos6thpi  16081  pigt3  16083  2logb9irr  16219  2logb9irrap  16225  ppiublem1  16303  konigsbergiedgwen  16942  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberglem4  16949