MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplbi2 Structured version   Unicode version

Theorem simplbi2 610
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 29132. (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 199 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 425 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360
This theorem is referenced by:  simplbi2com  1384  sspss  3435  neldif  3461  reuss2  3609  pssdifn0  3717  ordunidif  4664  eceqoveq  7045  infxpenlem  7933  ackbij1lem18  8155  isf32lem2  8272  ingru  8728  indpi  8822  nqereu  8844  algcvga  13108  pcprendvds  13252  restntr  17284  filcon  17953  filssufilg  17981  ufileu  17989  ufilen  18000  alexsubALTlem3  18118  blcld  18573  causs  19289  itg2addlem  19686  rplogsum  21259  sizeusglecusglem1  21531  esumpinfval  24498  sltres  25654  fdc  26491  ndmaovass  28158  elfz2z  28226  elfzmlbp  28228  elfzelfzelfz  28230  fzo1fzo0n0  28249  fzofzim  28257  swrdswrd  28331  swrdccatin1  28337  lstccats1fst  28395  cshweqdif2s  28403  usgra2pth  28447  onfrALTlem2  28804  3ornot23VD  29133  ordelordALTVD  29153  onfrALTlem2VD  29175  lshpcmp  29960  lfl1  30042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator