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

Theorem simplbi2 608
Description: Deduction eliminating a conjunct. Automatically derived from simplbi2VD 28622. (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 197 . 2  |-  ( ( ps  /\  ch )  ->  ph )
32ex 423 1  |-  ( ps 
->  ( ch  ->  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  simplbi2com  1364  sspss  3275  neldif  3301  reuss2  3448  pssdifn0  3515  ordunidif  4440  eceqoveq  6763  infxpenlem  7641  ackbij1lem18  7863  isf32lem2  7980  ingru  8437  indpi  8531  nqereu  8553  algcvga  12749  pcprendvds  12893  restntr  16912  filcon  17578  filssufilg  17606  ufileu  17614  ufilen  17625  alexsubALTlem3  17743  blcld  18051  causs  18724  itg2addlem  19113  rplogsum  20676  sltres  24318  intcont  25543  fdc  26455  ndmaovass  28066  onfrALTlem2  28311  3ornot23VD  28623  ordelordALTVD  28643  onfrALTlem2VD  28665  lshpcmp  29178  lfl1  29260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator