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  930  pm5.63dc  931  simplbi2com  1424  reuss2  3387  elni2  7234  elpq  9557  elfz0ubfz0  10024  elfzmlbp  10031  fzo1fzo0n0  10082  elfzo0z  10083  fzofzim  10087  elfzodifsumelfzo  10100  p1modz1  11690  dfgcd2  11897  algcvga  11927
  Copyright terms: Public domain W3C validator