Theorem mpbir3an 1205

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

Syntax hints:   ↔ wb 105   ∧ w3a 1004

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 1006

This theorem is referenced by:  limon  4613  limom  4714  issmo  6459  xpider  6780  aptap  8835  5eluz3  9800  1eluzge0  9813  2eluzge1  9815  0elunit  10226  1elunit  10227  fz0to3un2pr  10363  4fvwrd4  10380  fzo0to42pr  10471  xnn0nnen  10705  resqrexlemga  11606  fprodge0  12221  fprodge1  12223  sincos1sgn  12349  sincos2sgn  12350  igz  12970  qnnen  13075  strleun  13210  cnsubmlem  14616  cnsubglem  14617  cnsubrglem  14618  sinhalfpilem  15544  sincos4thpi  15593  sincos6thpi  15595  pigt3  15597  2logb9irr  15724  2logb9irrap  15730  konigsbergiedgwen  16364  konigsberglem1  16368  konigsberglem2  16369  konigsberglem3  16370  konigsberglem4  16371