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

Theorem mpbir3an 1180
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 1176 . 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 979
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 981
This theorem is referenced by:  limon  4524  limom  4625  issmo  6302  xpider  6619  aptap  8620  1eluzge0  9587  2eluzge1  9589  0elunit  9999  1elunit  10000  fz0to3un2pr  10136  4fvwrd4  10153  fzo0to42pr  10233  resqrexlemga  11045  fprodge0  11658  fprodge1  11660  sincos1sgn  11785  sincos2sgn  11786  igz  12385  qnnen  12445  strleun  12577  cnfldstr  13683  cnsubmlem  13698  cnsubglem  13699  cnsubrglem  13700  sinhalfpilem  14452  sincos4thpi  14501  sincos6thpi  14503  pigt3  14505  2logb9irr  14629  2logb9irrap  14635
  Copyright terms: Public domain W3C validator