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

Theorem simplbi2 385
Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.)
Hypothesis
Ref Expression
pm3.26bi2.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi2  |-  ( ps 
->  ( ch  ->  ph )
)

Proof of Theorem simplbi2
StepHypRef Expression
1 pm3.26bi2.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpri 133 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 115 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
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
This theorem is referenced by:  pm5.62dc  947  pm5.63dc  948  simplbi2com  1455  reuss2  3430  elni2  7331  elpq  9666  elfz0ubfz0  10143  elfzmlbp  10150  fzo1fzo0n0  10201  elfzo0z  10202  fzofzim  10206  elfzodifsumelfzo  10219  p1modz1  11819  dfgcd2  12033  algcvga  12069  pcprendvds  12308
  Copyright terms: Public domain W3C validator