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

Theorem mpbir3an 1179
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 1175 . 2 (𝜓𝜒𝜃)
5 mpbir3an.4 . 2 (𝜑 ↔ (𝜓𝜒𝜃))
64, 5mpbir 146 1 𝜑
Colors of variables: wff set class
Syntax hints:  wb 105  w3a 978
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 980
This theorem is referenced by:  limon  4508  limom  4609  issmo  6282  xpider  6599  1eluzge0  9550  2eluzge1  9552  0elunit  9960  1elunit  9961  fz0to3un2pr  10096  4fvwrd4  10113  fzo0to42pr  10193  resqrexlemga  11003  fprodge0  11616  fprodge1  11618  sincos1sgn  11743  sincos2sgn  11744  igz  12342  qnnen  12402  strleun  12532  sinhalfpilem  13845  sincos4thpi  13894  sincos6thpi  13896  pigt3  13898  2logb9irr  14022  2logb9irrap  14028
  Copyright terms: Public domain W3C validator