Theorem mpbir3an 1203

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

Syntax hints:   ↔ wb 105   ∧ w3a 1002

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 1004

This theorem is referenced by:  limon  4606  limom  4707  issmo  6445  xpider  6766  aptap  8813  1eluzge0  9786  2eluzge1  9788  0elunit  10199  1elunit  10200  fz0to3un2pr  10336  4fvwrd4  10353  fzo0to42pr  10443  xnn0nnen  10676  resqrexlemga  11555  fprodge0  12169  fprodge1  12171  sincos1sgn  12297  sincos2sgn  12298  igz  12918  qnnen  13023  strleun  13158  cnsubmlem  14563  cnsubglem  14564  cnsubrglem  14565  sinhalfpilem  15486  sincos4thpi  15535  sincos6thpi  15537  pigt3  15539  2logb9irr  15666  2logb9irrap  15672