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

Theorem mpbir3an 1164
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 1160 . 2  |-  ( ps 
/\  ch  /\  th )
5 mpbir3an.4 . 2  |-  ( ph  <->  ( ps  /\  ch  /\  th ) )
64, 5mpbir 145 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 104    /\ w3a 963
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 965
This theorem is referenced by:  limon  4436  limom  4534  issmo  6192  xpider  6507  1eluzge0  9395  2eluzge1  9397  0elunit  9798  1elunit  9799  4fvwrd4  9947  fzo0to42pr  10027  resqrexlemga  10826  sincos1sgn  11505  sincos2sgn  11506  qnnen  11978  strleun  12085  sinhalfpilem  12918  sincos4thpi  12967  sincos6thpi  12969  pigt3  12971  2logb9irr  13094  2logb9irrap  13100
  Copyright terms: Public domain W3C validator