Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpbir3an GIF version

Theorem mpbir3an 1163
 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
StepHypRef Expression
1 mpbir3an.1 . . 3 𝜓
2 mpbir3an.2 . . 3 𝜒
3 mpbir3an.3 . . 3 𝜃
41, 2, 33pm3.2i 1159 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 145 1 𝜑
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   ∧ w3a 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 964 This theorem is referenced by:  limon  4429  limom  4527  issmo  6185  xpider  6500  1eluzge0  9383  2eluzge1  9385  0elunit  9783  1elunit  9784  4fvwrd4  9931  fzo0to42pr  10011  resqrexlemga  10809  sincos1sgn  11484  sincos2sgn  11485  qnnen  11957  strleun  12064  sinhalfpilem  12896  sincos4thpi  12945  sincos6thpi  12947  pigt3  12949
 Copyright terms: Public domain W3C validator