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  4609  limom  4710  issmo  6449  xpider  6770  aptap  8823  5eluz3  9788  1eluzge0  9801  2eluzge1  9803  0elunit  10214  1elunit  10215  fz0to3un2pr  10351  4fvwrd4  10368  fzo0to42pr  10458  xnn0nnen  10692  resqrexlemga  11577  fprodge0  12191  fprodge1  12193  sincos1sgn  12319  sincos2sgn  12320  igz  12940  qnnen  13045  strleun  13180  cnsubmlem  14585  cnsubglem  14586  cnsubrglem  14587  sinhalfpilem  15508  sincos4thpi  15557  sincos6thpi  15559  pigt3  15561  2logb9irr  15688  2logb9irrap  15694