Theorem mpbir3an 1169

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

Syntax hints:   ↔ wb 104   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  limon  4489  limom  4590  issmo  6252  xpider  6568  1eluzge0  9508  2eluzge1  9510  0elunit  9918  1elunit  9919  fz0to3un2pr  10054  4fvwrd4  10071  fzo0to42pr  10151  resqrexlemga  10961  fprodge0  11574  fprodge1  11576  sincos1sgn  11701  sincos2sgn  11702  igz  12300  qnnen  12360  strleun  12479  sinhalfpilem  13312  sincos4thpi  13361  sincos6thpi  13363  pigt3  13365  2logb9irr  13489  2logb9irrap  13495