Theorem mpbir3an 1184

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

Syntax hints:   ↔ wb 105   ∧ w3a 983

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 985

This theorem is referenced by:  limon  4582  limom  4683  issmo  6404  xpider  6723  aptap  8765  1eluzge0  9737  2eluzge1  9739  0elunit  10150  1elunit  10151  fz0to3un2pr  10287  4fvwrd4  10304  fzo0to42pr  10393  xnn0nnen  10626  resqrexlemga  11500  fprodge0  12114  fprodge1  12116  sincos1sgn  12242  sincos2sgn  12243  igz  12863  qnnen  12968  strleun  13103  cnsubmlem  14507  cnsubglem  14508  cnsubrglem  14509  sinhalfpilem  15430  sincos4thpi  15479  sincos6thpi  15481  pigt3  15483  2logb9irr  15610  2logb9irrap  15616