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  4530  limom  4631  issmo  6313  xpider  6632  aptap  8637  1eluzge0  9604  2eluzge1  9606  0elunit  10016  1elunit  10017  fz0to3un2pr  10153  4fvwrd4  10170  fzo0to42pr  10250  resqrexlemga  11064  fprodge0  11677  fprodge1  11679  sincos1sgn  11804  sincos2sgn  11805  igz  12406  qnnen  12482  strleun  12616  cnfldstr  13866  cnsubmlem  13881  cnsubglem  13882  cnsubrglem  13883  sinhalfpilem  14672  sincos4thpi  14721  sincos6thpi  14723  pigt3  14725  2logb9irr  14849  2logb9irrap  14855
  Copyright terms: Public domain W3C validator