Theorem mpbir3an 1181

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

Syntax hints:   ↔ wb 105   ∧ w3a 980

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 982

This theorem is referenced by:  limon  4530  limom  4631  issmo  6314  xpider  6633  aptap  8638  1eluzge0  9606  2eluzge1  9608  0elunit  10018  1elunit  10019  fz0to3un2pr  10155  4fvwrd4  10172  fzo0to42pr  10252  resqrexlemga  11067  fprodge0  11680  fprodge1  11682  sincos1sgn  11807  sincos2sgn  11808  igz  12409  qnnen  12485  strleun  12619  cnfldstr  13883  cnsubmlem  13898  cnsubglem  13899  cnsubrglem  13900  sinhalfpilem  14689  sincos4thpi  14738  sincos6thpi  14740  pigt3  14742  2logb9irr  14866  2logb9irrap  14872