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

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  |-  ps
mpbir3an.2  |-  ch
mpbir3an.3  |-  th
mpbir3an.4  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
Assertion
Ref Expression
mpbir3an  |-  ph

Proof of Theorem mpbir3an
StepHypRef Expression
1 mpbir3an.1 . . 3  |-  ps
2 mpbir3an.2 . . 3  |-  ch
3 mpbir3an.3 . . 3  |-  th
41, 2, 33pm3.2i 1177 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 146 1  |-  ph
Colors of variables: wff set class
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  4527  limom  4628  issmo  6307  xpider  6624  aptap  8626  1eluzge0  9593  2eluzge1  9595  0elunit  10005  1elunit  10006  fz0to3un2pr  10142  4fvwrd4  10159  fzo0to42pr  10239  resqrexlemga  11051  fprodge0  11664  fprodge1  11666  sincos1sgn  11791  sincos2sgn  11792  igz  12391  qnnen  12456  strleun  12588  cnfldstr  13833  cnsubmlem  13848  cnsubglem  13849  cnsubrglem  13850  sinhalfpilem  14615  sincos4thpi  14664  sincos6thpi  14666  pigt3  14668  2logb9irr  14792  2logb9irrap  14798
  Copyright terms: Public domain W3C validator