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  4637  limom  4738  issmo  6521  xpider  6842  aptap  8929  5eluz3  9899  1eluzge0  9912  2eluzge1  9914  0elunit  10325  1elunit  10326  fz0to3un2pr  10464  4fvwrd4  10481  fzo0to42pr  10572  xnn0nnen  10806  resqrexlemga  11716  fprodge0  12331  fprodge1  12333  sincos1sgn  12459  sincos2sgn  12460  igz  13080  ballotfilem2  13153  qnnen  13203  strleun  13338  cnsubmlem  14775  cnsubglem  14776  cnsubrglem  14777  sinhalfpilem  15705  sincos4thpi  15754  sincos6thpi  15756  pigt3  15758  2logb9irr  15885  2logb9irrap  15891  konigsbergiedgwen  16528  konigsberglem1  16532  konigsberglem2  16533  konigsberglem3  16534  konigsberglem4  16535