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

Theorem simplbi2 383
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 132 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 114 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
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
This theorem is referenced by:  pm5.62dc  940  pm5.63dc  941  simplbi2com  1437  reuss2  3407  elni2  7276  elpq  9607  elfz0ubfz0  10081  elfzmlbp  10088  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzodifsumelfzo  10157  p1modz1  11756  dfgcd2  11969  algcvga  12005  pcprendvds  12244
  Copyright terms: Public domain W3C validator