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  4611  limom  4712  issmo  6454  xpider  6775  aptap  8830  5eluz3  9795  1eluzge0  9808  2eluzge1  9810  0elunit  10221  1elunit  10222  fz0to3un2pr  10358  4fvwrd4  10375  fzo0to42pr  10466  xnn0nnen  10700  resqrexlemga  11585  fprodge0  12200  fprodge1  12202  sincos1sgn  12328  sincos2sgn  12329  igz  12949  qnnen  13054  strleun  13189  cnsubmlem  14595  cnsubglem  14596  cnsubrglem  14597  sinhalfpilem  15518  sincos4thpi  15567  sincos6thpi  15569  pigt3  15571  2logb9irr  15698  2logb9irrap  15704