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  4635  limom  4736  issmo  6519  xpider  6840  aptap  8924  5eluz3  9893  1eluzge0  9906  2eluzge1  9908  0elunit  10319  1elunit  10320  fz0to3un2pr  10457  4fvwrd4  10474  fzo0to42pr  10565  xnn0nnen  10799  resqrexlemga  11706  fprodge0  12321  fprodge1  12323  sincos1sgn  12449  sincos2sgn  12450  igz  13070  ballotfilem2  13140  qnnen  13180  strleun  13315  cnsubmlem  14724  cnsubglem  14725  cnsubrglem  14726  sinhalfpilem  15654  sincos4thpi  15703  sincos6thpi  15705  pigt3  15707  2logb9irr  15834  2logb9irrap  15840  konigsbergiedgwen  16477  konigsberglem1  16481  konigsberglem2  16482  konigsberglem3  16483  konigsberglem4  16484