Theorem mpbir3an 1182

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

Syntax hints:   ↔ wb 105   ∧ w3a 981

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 983

This theorem is referenced by:  limon  4565  limom  4666  issmo  6381  xpider  6700  aptap  8730  1eluzge0  9702  2eluzge1  9704  0elunit  10115  1elunit  10116  fz0to3un2pr  10252  4fvwrd4  10269  fzo0to42pr  10356  xnn0nnen  10589  resqrexlemga  11378  fprodge0  11992  fprodge1  11994  sincos1sgn  12120  sincos2sgn  12121  igz  12741  qnnen  12846  strleun  12980  cnsubmlem  14384  cnsubglem  14385  cnsubrglem  14386  sinhalfpilem  15307  sincos4thpi  15356  sincos6thpi  15358  pigt3  15360  2logb9irr  15487  2logb9irrap  15493