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  4605  limom  4706  issmo  6440  xpider  6761  aptap  8805  1eluzge0  9777  2eluzge1  9779  0elunit  10190  1elunit  10191  fz0to3un2pr  10327  4fvwrd4  10344  fzo0to42pr  10434  xnn0nnen  10667  resqrexlemga  11542  fprodge0  12156  fprodge1  12158  sincos1sgn  12284  sincos2sgn  12285  igz  12905  qnnen  13010  strleun  13145  cnsubmlem  14550  cnsubglem  14551  cnsubrglem  14552  sinhalfpilem  15473  sincos4thpi  15522  sincos6thpi  15524  pigt3  15526  2logb9irr  15653  2logb9irrap  15659